hindley milner inference :D
This commit is contained in:
@@ -2,6 +2,7 @@
|
|||||||
module Core.HindleyMilner
|
module Core.HindleyMilner
|
||||||
( infer
|
( infer
|
||||||
, Context'
|
, Context'
|
||||||
|
, TypeError(..)
|
||||||
)
|
)
|
||||||
where
|
where
|
||||||
----------------------------------------------------------------------------------
|
----------------------------------------------------------------------------------
|
||||||
@@ -18,7 +19,12 @@ type Context b = [(b, Type)]
|
|||||||
|
|
||||||
type Context' = Context Name
|
type Context' = Context Name
|
||||||
|
|
||||||
infer :: Context' -> Expr' -> Maybe Type
|
-- TODO: Errorful monad?
|
||||||
|
data TypeError = TyErrCouldNotUnify Type Type
|
||||||
|
| TyErrRecursiveType Name Type
|
||||||
|
deriving Show
|
||||||
|
|
||||||
|
infer :: Context' -> Expr' -> Either TypeError Type
|
||||||
infer g e = foldr (uncurry subst) t <$> unify cs where
|
infer g e = foldr (uncurry subst) t <$> unify cs where
|
||||||
(t,cs) = gather g e
|
(t,cs) = gather g e
|
||||||
|
|
||||||
@@ -47,12 +53,12 @@ uniqueVar = do
|
|||||||
addConstraint :: Type -> Type -> State ([Constraint], Int) ()
|
addConstraint :: Type -> Type -> State ([Constraint], Int) ()
|
||||||
addConstraint t u = _1 %= ((t, u):)
|
addConstraint t u = _1 %= ((t, u):)
|
||||||
|
|
||||||
unify :: [Constraint] -> Maybe Context'
|
unify :: [Constraint] -> Either TypeError Context'
|
||||||
unify = go mempty where
|
unify = go mempty where
|
||||||
go :: Context' -> [Constraint] -> Maybe Context'
|
go :: Context' -> [Constraint] -> Either TypeError Context'
|
||||||
|
|
||||||
-- nothing left! return accumulator
|
-- nothing left! return accumulated context
|
||||||
go g [] = Just g
|
go g [] = Right g
|
||||||
|
|
||||||
go g (c:cs) = case c of
|
go g (c:cs) = case c of
|
||||||
-- primitives may of course unify with themselves
|
-- primitives may of course unify with themselves
|
||||||
@@ -69,10 +75,11 @@ unify = go mempty where
|
|||||||
-- two functions may be unified if their domain and codomain unify
|
-- two functions may be unified if their domain and codomain unify
|
||||||
(a :-> b, x :-> y) -> go g $ (a,x) : (b,y) : cs
|
(a :-> b, x :-> y) -> go g $ (a,x) : (b,y) : cs
|
||||||
|
|
||||||
_ -> Nothing
|
-- anything else is a failure :(
|
||||||
|
(t,u) -> Left $ TyErrCouldNotUnify t u
|
||||||
|
|
||||||
unifyTV :: Context' -> Name -> Type -> [Constraint] -> Maybe Context'
|
unifyTV :: Context' -> Name -> Type -> [Constraint] -> Either TypeError Context'
|
||||||
unifyTV g x t cs | occurs t = Nothing
|
unifyTV g x t cs | occurs t = Left $ TyErrRecursiveType x t
|
||||||
| otherwise = go g' substed
|
| otherwise = go g' substed
|
||||||
where
|
where
|
||||||
g' = (x,t) : g
|
g' = (x,t) : g
|
||||||
|
|||||||
@@ -50,7 +50,6 @@ data Expr b = Var Name
|
|||||||
| Let Rec [Binding b] (Expr b)
|
| Let Rec [Binding b] (Expr b)
|
||||||
| App (Expr b) (Expr b)
|
| App (Expr b) (Expr b)
|
||||||
| Lit Lit
|
| Lit Lit
|
||||||
| Type Type
|
|
||||||
deriving (Show, Read, Lift)
|
deriving (Show, Read, Lift)
|
||||||
|
|
||||||
deriving instance (Eq b) => Eq (Expr b)
|
deriving instance (Eq b) => Eq (Expr b)
|
||||||
@@ -59,7 +58,6 @@ data Type = TyInt
|
|||||||
| TyFun
|
| TyFun
|
||||||
| TyVar Name
|
| TyVar Name
|
||||||
| TyApp Type Type
|
| TyApp Type Type
|
||||||
-- | TyConApp TyCon [Type]
|
|
||||||
deriving (Show, Read, Lift, Eq)
|
deriving (Show, Read, Lift, Eq)
|
||||||
|
|
||||||
type TyCon = Name
|
type TyCon = Name
|
||||||
|
|||||||
Reference in New Issue
Block a user