implementation module check
import StdEnv
-import Data.Either
-import Data.List
+
+import qualified Data.Map as DM
+from Data.Map import instance Functor (Map k)
+import qualified Data.Set as DS
import Data.Functor
import Data.Func
+import Data.Either
+import Data.List
import Data.Maybe
-import Data.Monoid
import Control.Applicative
import Control.Monad
import Control.Monad.Trans
-import Control.Monad.RWST
-import qualified Data.Map as DM
-from Data.Map import instance Functor (Map k)
+import qualified Control.Monad.State as MS
+import Control.Monad.State => qualified gets, put, modify
+import Control.Monad.RWST => qualified put
import ast
-//Start = runRWST (infer (AST [(Function ['s','t','a','r','t'] [] (Lit (Int 42)))])
-Start = runRWST (infer (TypeEnv 'DM'.newMap) t) [] {tiSupply=0,tiSubst='DM'.newMap}
+check :: AST -> Either [String] (AST, [([Char], Scheme)])
+check (AST fs) = pure (AST fs, [])/*case inferAST preamble fs of
+ Left e = Left e
+ Right s = Right (AST fs, 'DM'.toList s)
where
-// t = Function ['start'] [] (Lit (Int 42))
- t =
- [Function ['id'] [] (Lit (Int 42))
- ,Function ['start'] [] (App (Var ['id']) (Lit (Int 42)))
+ preamble = 'DM'.fromList
+ [(['if'], Forall [['a']] $ TFun TBool $ TFun (TVar ['a']) $ TFun (TVar ['a']) $ TVar ['a'])
+ ,(['eq'], Forall [] $ TFun TInt $ TFun TInt TBool)
+ ,(['mul'], Forall [] $ TFun TInt $ TFun TInt TInt)
+ ,(['div'], Forall [] $ TFun TInt $ TFun TInt TInt)
+ ,(['add'], Forall [] $ TFun TInt $ TFun TInt TInt)
+ ,(['sub'], Forall [] $ TFun TInt $ TFun TInt TInt)
]
+*/
+
+:: TypeEnv :== 'DM'.Map [Char] Scheme
+:: Constraint :== (Type, Type)
+:: Subst :== 'DM'.Map [Char] Type
+:: Unifier :== (Subst, [Constraint])
+:: Infer a :== RWST TypeEnv [Constraint] InferState (Either [String]) a
+:: InferState = { count :: Int }
+:: Scheme = Forall [[Char]] Type
+:: Solve a :== StateT Unifier (Either [String]) a
-check :: AST -> Either [String] AST
-check (AST fs) = case sortBy (on (>) isStart) fs of
- [(Function ['start'] as _):rest]
- = case runRWST (infer (TypeEnv 'DM'.newMap) fs) [] {tiSupply=0,tiSubst='DM'.newMap} of
- Left e = Left e
- Right _ = Right (AST fs)
- _ = Left ["No start function defined"]
+nullSubst :: Subst
+nullSubst = 'DM'.newMap
+
+uni :: Type Type -> Infer ()
+uni t1 t2 = tell [(t1, t2)]
+
+inEnv :: ([Char], Scheme) (Infer a) -> Infer a
+inEnv (x, sc) m = local (\e->'DM'.put x sc $ 'DM'.del x e) m
+
+letters :: [[Char]]
+letters = [1..] >>= flip replicateM ['a'..'z']
+
+fresh :: Infer Type
+fresh = get >>= \s=:{count}->'Control.Monad.RWST'.put {s & count=count + 1} >>| pure (TVar $ letters !! count)
+
+class Substitutable a
where
- isStart a = a=:(Function ['start'] [] _)
-
-instance < Bool where
- < False True = True
- < _ _ = False
-
-:: Type
- = TVar [Char]
- | TInt
- | TBool
- | TChar
- | TFun Type Type
-
-instance == Type where
- (==) (TVar a) (TVar b) = a == b
- (==) TInt TInt = True
- (==) TBool TBool = True
- (==) TChar TChar = True
- (==) (TFun a1 a2) (TFun b1 b2) = a1 == b1 && a2 == b2
- (==) _ _ = False
-
-instance toString Type where
- toString (TVar s) = toString s
- toString TInt = "Int"
- toString TBool = "Bool"
- toString TChar = "Char"
- toString (TFun t1 t2) = toString t1 +++ " -> " +++ toString t2
-
-:: Scheme = Scheme [[Char]] Type
-class Types a where
- ftv :: a -> [[Char]]
apply :: Subst a -> a
+ ftv :: a -> [[Char]]
-instance Types Type where
- ftv (TVar n) = [n]
- ftv TInt = []
- ftv TBool = []
- ftv TChar = []
- ftv (TFun t1 t2) = union (ftv t1) (ftv t2)
+instance Substitutable Type
+where
+ apply s t=:(TVar a) = maybe t id $ 'DM'.get a s
+ apply s (TFun t1 t2) = TFun (apply s t1) (apply s t2)
+ apply _ t = t
- apply s (TVar n) = case 'DM'.get n s of
- Nothing = TVar n
- Just t = t
- apply s (TFun t1 t2) = TFun (apply s t1) (apply s t2)
- apply s t = t
+ ftv (TVar a) = [a]
+ ftv (TFun t1 t2) = union (ftv t1) (ftv t2)
+ ftv t = []
-instance Types Scheme where
- ftv (Scheme vars t) = difference (ftv t) vars
- apply s (Scheme vars t) = Scheme vars (apply (foldr 'DM'.del s vars) t)
+instance Substitutable Scheme
+where
+ apply s (Forall as t) = Forall as $ apply (foldr 'DM'.del s as) t
+ ftv (Forall as t) = difference (ftv t) as
-instance Types [a] | Types a where
- ftv l = foldr union [] (map ftv l)
- apply s l = map (apply s) l
+instance Substitutable [a] | Substitutable a
+where
+ apply s ls = map (apply s) ls
+ ftv t = foldr (union o ftv) [] t
-:: Subst :== 'DM'.Map [Char] Type
-composeSubst s1 s2 = 'DM'.union ((apply s1) <$> s2) s1
+instance Substitutable TypeEnv where
+ apply s env = fmap (apply s) env
+ ftv env = ftv $ 'DM'.elems env
-:: TypeEnv = TypeEnv ('DM'.Map [Char] Scheme)
-remove :: TypeEnv [Char] -> TypeEnv
-remove (TypeEnv env) var = TypeEnv ('DM'.del var env)
+instance Substitutable Constraint where
+ apply s (t1, t2) = (apply s t1, apply s t2)
+ ftv (t1, t2) = union (ftv t1) (ftv t2)
-instance Types TypeEnv where
- ftv (TypeEnv env) = ftv ('DM'.elems env)
- apply s (TypeEnv env) = TypeEnv (apply s <$> env)
+instantiate :: Scheme -> Infer Type
+instantiate (Forall as t) = mapM (const fresh) as
+ >>= \as`->let s = 'DM'.fromList $ zip2 as as` in pure $ apply s t
generalize :: TypeEnv Type -> Scheme
-generalize env t = Scheme (difference (ftv t) (ftv env)) t
-
-:: TI a :== RWST TIEnv () TIState (Either [String]) a
-:: TIState = {tiSupply :: Int, tiSubst :: Subst}
-:: TIEnv :== [Int]
-
-mgu :: Type Type -> TI Subst
-mgu (TFun l r) (TFun l` r`) = composeSubst <$> mgu l l` <*> mgu r r`
-mgu (TVar u) t = varBind u t
-mgu t (TVar u) = varBind u t
-mgu TInt TInt = pure 'DM'.newMap
-mgu TBool TBool = pure 'DM'.newMap
-mgu TChar TChar = pure 'DM'.newMap
-mgu t1 t2 = liftT (Left ["cannot unify: " +++ toString t1 +++ " with " +++ toString t2])
-
-varBind :: [Char] Type -> TI Subst
-varBind u t
- | t == TVar u = pure 'DM'.newMap
- | isMember u (ftv t) = liftT (Left ["occur check fails: " +++ toString u +++ " vs. " +++ toString t])
- = pure ('DM'.singleton u t)
-
-newTyVar :: [Char] -> TI Type
-newTyVar prefix
- = get
- >>= \t->put {t & tiSupply=t.tiSupply+1}
- >>| pure (TVar (prefix ++ fromString (toString t.tiSupply)))
-
-instantiate :: Scheme -> TI Type
-instantiate (Scheme vars t)
- = mapM (\_->newTyVar ['a']) vars
- >>= \nvars->pure (apply ('DM'.fromList (zip2 vars nvars)) t)
-
-class infer a :: TypeEnv a -> TI (Subst, Type)
-
-instance infer Value where
- infer _ (Int _) = pure ('DM'.newMap, TInt)
- infer _ (Bool _) = pure ('DM'.newMap, TBool)
- infer _ (Char _) = pure ('DM'.newMap, TChar)
-
-instance infer Expression where
- infer e (Lit a) = infer e a
- infer (TypeEnv env) (Var v) = case 'DM'.get v env of
- Nothing = liftT (Left ["unbound variable: " +++ toString v])
- Just s = instantiate s >>= \t->pure ('DM'.newMap, t)
- infer env (App e1 e2)
- = newTyVar ['a']
- >>= \tv ->infer env e1
- >>= \(s1, t1)->infer (apply s1 env) e2
- >>= \(s2, t2)->mgu (apply s2 t1) (TFun t2 tv)
- >>= \s3->pure (composeSubst s3 (composeSubst s2 s1), apply s3 tv)
- infer env (Lambda s e)
- = newTyVar ['l']
- >>= \tv->
- let (TypeEnv env`) = remove env s
- env`` = TypeEnv ('DM'.union env` ('DM'.singleton s (Scheme [] tv)))
- in infer env`` e
- >>= \(s1, t1)->pure (s1, TFun (apply s1 tv) t1)
-
-instance infer [Function] where
- infer env [] = pure ('DM'.newMap, TInt)
- infer env [Function name args body:rest]
- = infer env (foldr Lambda body args) >>= \(s1, t1)->
- let (TypeEnv env`) = remove env name
- t` = generalize (apply s1 env) t1
- env`` = TypeEnv ('DM'.put name t` env`)
- in infer (apply s1 env``) rest >>= \(s2, t2)->pure (composeSubst s1 s2, t2)
-
-typeInference :: ('DM'.Map [Char] Scheme) Expression -> TI Type
-typeInference env e = uncurry apply <$> infer (TypeEnv env) e
+generalize env t = Forall (difference (ftv t) (ftv env)) t
+
+//:: Expression
+// = Lit Value
+// | Var [Char]
+// | App Expression Expression
+// | Lambda [Char] Expression
+// | Builtin [Char] [Expression]
+inferExpr :: TypeEnv Expression -> Either [String] Scheme
+inferExpr env ex = case runRWST (infer ex) env {count=0} of
+ Left e = Left e
+ Right (ty, st, cs) = case runStateT solver ('DM'.newMap, cs) of
+ Left e = Left e
+ Right (s, _) = Right (closeOver (apply s ty))
+
+closeOver :: Type -> Scheme
+closeOver t = normalize (generalize 'DM'.newMap t)
+
+normalize :: Scheme -> Scheme
+normalize t = t
+
+inferAST :: TypeEnv [Function] -> Either [String] TypeEnv
+inferAST env [] = Right env
+inferAST env [Function name args body:rest] = case inferExpr env (foldr Lambda body args) of
+ Left e = Left e
+ Right ty = inferAST ('DM'.put name ty env) rest
+
+inferFunc :: [Function] -> Infer ()
+inferFunc [] = pure ()
+inferFunc [Function name args body:rest]
+ = ask
+ >>= \en->infer (foldr Lambda body args)
+ >>= \t1->inEnv (name, generalize en t1) (inferFunc rest)
+ >>= \_->pure ()
+
+infer :: Expression -> Infer Type
+infer (Lit v) = case v of
+ Int _ = pure TInt
+ Bool _ = pure TBool
+ Char _ = pure TChar
+infer (Var s) = asks ('DM'.get s)
+ >>= maybe (liftT $ Left ["Unbound variable " +++ toString s]) instantiate
+infer (App e1 e2)
+ = infer e1
+ >>= \t1->infer e2
+ >>= \t2->fresh
+ >>= \tv->uni t1 (TFun t2 tv)
+ >>| pure tv
+infer (Lambda s e)
+ = fresh
+ >>= \tv->inEnv (s, Forall [] tv) (infer e)
+ >>= \t-> pure (TFun tv t)
+//infer (Let x e1 e2)
+// = ask
+// >>= \en->infer e1
+// >>= \t1->inEnv (x, generalize en t1) (infer e2)
+
+unifies :: Type Type -> Solve Unifier
+unifies TInt TInt = pure ('DM'.newMap, [])
+unifies TBool TBool = pure ('DM'.newMap, [])
+unifies TChar TChar = pure ('DM'.newMap, [])
+unifies (TVar a) (TVar b)
+ | a == b = pure ('DM'.newMap, [])
+unifies (TVar v) t = tbind v t
+unifies t (TVar v) = tbind v t
+unifies (TFun t1 t2) (TFun t3 t4) = unifyMany [t1, t2] [t3, t4]
+unifies t1 t2 = liftT $ Left ["Cannot unify " +++ toString t1 +++ " with " +++ toString t2]
+
+unifyMany :: [Type] [Type] -> Solve Unifier
+unifyMany [] [] = pure ('DM'.newMap, [])
+unifyMany [t1:ts1] [t2:ts2] = unifies t1 t2
+ >>= \(su1, cs1)->unifyMany (apply su1 ts1) (apply su1 ts2)
+ >>= \(su2, cs2)->pure (su2 `compose` su1, cs1 ++ cs2)
+unifyMany t1 t2 = liftT $ Left ["Length difference in unifyMany"]
+
+(`compose`) infix 1 :: Subst Subst -> Subst
+(`compose`) s1 s2 = 'DM'.union (apply s1 <$> s2) s1
+
+tbind :: [Char] Type -> Solve Unifier
+tbind a (TVar b)
+ | a == b = pure ('DM'.newMap, [])
+tbind a t
+ | occursCheck a t = liftT $ Left ["Infinite type " +++ toString a +++ toString t]
+ = pure $ ('DM'.singleton a t, [])
+
+occursCheck :: [Char] a -> Bool | Substitutable a
+occursCheck a t = isMember a $ ftv t
+
+solver :: Solve Subst
+solver = getState >>= \(su, cs)->case cs of
+ [] = pure su
+ [(t1, t2):cs0] = unifies t1 t2
+ >>= \(su1, cs1)->'MS'.put (su1 `compose` su, cs1 ++ (apply su1 cs0))
+ >>| solver
repositories / minfp.git / blobdiff