| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
TypeChecker.HindleyMilner
Contents
Synopsis
- type Infer = ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity))
- data TypeError where
- Unreachable :: TypeError
- UnboundVar :: Identifier -> TypeError
- Infinite :: IntVar -> UType -> TypeError
- ImpossibleBinOpApplication :: UType -> UType -> TypeError
- ImpossibleUnOpApplication :: UType -> TypeError
- Mismatch :: TypeF UType -> TypeF UType -> TypeError
- type UType = UTerm TypeF IntVar
- type Polytype = Poly Type
- applyBindings :: UType -> Infer UType
- generalize :: UType -> Infer UPolytype
- toPolytype :: UPolytype -> Polytype
- toUType :: Type -> UType
- withBinding :: MonadReader Ctx m => Identifier -> UPolytype -> m a -> m a
- fresh :: Infer UType
- data Poly t = Forall [Identifier] t
- data UTerm (t :: Type -> Type) v where
- (=:=) :: UType -> UType -> Infer UType
- lookup :: Identifier -> Infer UType
- data TypeF a
- mkVarName :: String -> IntVar -> Identifier
Documentation
Constructors
| Unreachable :: TypeError | |
| UnboundVar :: Identifier -> TypeError | |
| Infinite :: IntVar -> UType -> TypeError | |
| ImpossibleBinOpApplication :: UType -> UType -> TypeError | |
| ImpossibleUnOpApplication :: UType -> TypeError | |
| Mismatch :: TypeF UType -> TypeF UType -> TypeError |
generalize :: UType -> Infer UPolytype Source #
toPolytype :: UPolytype -> Polytype Source #
withBinding :: MonadReader Ctx m => Identifier -> UPolytype -> m a -> m a Source #
Constructors
| Forall [Identifier] t |
data UTerm (t :: Type -> Type) v where #
The type of terms generated by structures t over variables
v. The structure type should implement Unifiable and the
variable type should implement Variable.
The Show instance doesn't show the constructors, in order to
improve legibility for large terms.
All the category theoretic instances (Functor, Foldable,
Traversable,...) are provided because they are often useful;
however, beware that since the implementations must be pure,
they cannot read variables bound in the current context and
therefore can create incoherent results. Therefore, you should
apply the current bindings before using any of the functions
provided by those classes.
Bundled Patterns
| pattern UTVar :: Identifier -> UType | |
| pattern UTUnit :: UType | |
| pattern UTBool :: UType | |
| pattern UTInt :: UType | |
| pattern UTFun :: UType -> UType -> UType |
Instances
| Foldable t => Foldable (UTerm t) | |
Defined in Control.Unification.Types Methods fold :: Monoid m => UTerm t m -> m # foldMap :: Monoid m => (a -> m) -> UTerm t a -> m # foldMap' :: Monoid m => (a -> m) -> UTerm t a -> m # foldr :: (a -> b -> b) -> b -> UTerm t a -> b # foldr' :: (a -> b -> b) -> b -> UTerm t a -> b # foldl :: (b -> a -> b) -> b -> UTerm t a -> b # foldl' :: (b -> a -> b) -> b -> UTerm t a -> b # foldr1 :: (a -> a -> a) -> UTerm t a -> a # foldl1 :: (a -> a -> a) -> UTerm t a -> a # elem :: Eq a => a -> UTerm t a -> Bool # maximum :: Ord a => UTerm t a -> a # minimum :: Ord a => UTerm t a -> a # | |
| Traversable t => Traversable (UTerm t) | |
| Functor t => Applicative (UTerm t) | |
| Functor t => Functor (UTerm t) | |
| Functor t => Monad (UTerm t) | |
| (Show v, Show (t (UTerm t v))) => Show (UTerm t v) | |