1 implementation module check
12 import Control.Monad.Trans
13 import Control.Monad.State
15 import qualified Data.Map
16 from Data.Map import instance Functor (Map k)
21 check :: [Function] -> Either [String] Expression
23 # dups = filter (\x->length x > 1) (groupBy (\(Function i _ _) (Function j _ _)->i == j) fs)
24 | length dups > 0 = Left ["Duplicate functions: ":[toString n\\[(Function n _ _):_]<-dups]]
25 = case partition (\a->a=:(Function ['start'] _ _)) fs of
26 ([], _) = Left ["No start function defined"]
27 ([Function _ [] e], fs)
28 # e = foldr (\(Function i a e)->Let i (mkLambda a e)) e fs
29 = case runInfer (infer 'Data.Map'.newMap e) of
32 = Left [printToString s]
33 ([Function _ _ _], _) = Left ["Start cannot have arguments"]
35 mkLambda :: [[Char]] Expression -> Expression
37 mkLambda [a:as] e = Lambda a (mkLambda as e)
40 derive gPrint Scheme, Type
43 :: Scheme = Forall [[Char]] Type
44 :: TypeEnv :== 'Data.Map'.Map [Char] Scheme
45 :: Subst :== 'Data.Map'.Map [Char] Type
46 nullSubst = 'Data.Map'.newMap
48 :: Infer a :== StateT [Int] (Either [String]) a
49 runInfer :: (Infer (Subst, Type)) -> Either [String] Scheme
50 runInfer i = uncurry closeOver <$> evalStateT i [0..]
52 closeOver :: Subst Type -> Scheme
53 closeOver sub ty = normalize (generalize 'Data.Map'.newMap (apply sub ty))
55 normalize :: Scheme -> Scheme
57 // normalize (Forall ts body) = Forall (snd <$> ord) (normtype body)
59 // ord = zip2 (removeDup $ fv body) (fmap letters)
62 // fv (TFun a b) = fv a ++ fv b
65 // normtype (TFun a b) = TFun (normtype a) (normtype b)
66 // normtype (TCon a) = TCon a
67 // normtype (TVar a) =
68 // case lookup a ord of
70 // Nothing = Left ["type variable not in signature"]
73 fresh = getState >>= \[s:ss]->put ss >>| pure (TVar (['v':[c\\c<-:toString s]]))
75 compose :: Subst Subst -> Subst
76 compose s1 s2 = 'Data.Map'.union (apply s1 <$> s2) s1
78 class Substitutable a where
82 instance Substitutable Type where
83 apply s t=:(TVar v) = 'Data.Map'.findWithDefault t v s
84 apply s (TFun t1 t2) = on TFun (apply s) t1 t2
88 ftv (TFun t1 t2) = on union ftv t1 t2
91 instance Substitutable Scheme where
92 apply s (Forall as t) = Forall as $ apply (foldr 'Data.Map'.del s as) t
93 ftv (Forall as t) = difference (ftv t) (removeDup as)
95 instance Substitutable TypeEnv where
96 apply s env = apply s <$> env
97 ftv env = ftv ('Data.Map'.elems env)
99 instance Substitutable [a] | Substitutable a where
100 apply s l = apply s <$> l
101 ftv t = foldr (union o ftv) [] t
103 occursCheck :: [Char] -> (a -> Bool) | Substitutable a
104 occursCheck a = isMember a o ftv
106 unify :: Type Type -> Infer Subst
107 unify (TFun l r) (TFun l` r`)
109 >>= \s1->on unify (apply s1) r r`
110 >>= \s2->pure (compose s1 s2)
111 unify (TVar a) t = bind a t
112 unify t (TVar a) = bind a t
113 unify TInt TInt = pure nullSubst
114 unify TBool TBool = pure nullSubst
115 unify t1 t2 = liftT (Left ["Cannot unify: ", toString t1, " with ", toString t2])
117 bind :: [Char] Type -> Infer Subst
118 bind a (TVar t) | a == t = pure nullSubst
120 | occursCheck a t = liftT (Left ["Infinite type: ", toString a, " and ", toString t])
121 = pure ('Data.Map'.singleton a t)
123 instantiate :: Scheme -> Infer Type
124 instantiate (Forall as t)
125 = sequence [fresh\\_<-as]
126 >>= \as`->pure (apply ('Data.Map'.fromList $ zip2 as as`) t)
128 generalize :: TypeEnv Type -> Scheme
129 generalize env t = Forall (difference (ftv t) (ftv env)) t
131 infer :: TypeEnv Expression -> Infer (Subst, Type)
132 infer env (Lit (Int _)) = pure (nullSubst, TInt)
133 infer env (Lit (Bool _)) = pure (nullSubst, TBool)
134 infer env (Var x) = case 'Data.Map'.get x env of
135 Nothing = liftT (Left ["Unbound variable: ", toString x])
136 Just s = tuple nullSubst <$> instantiate s
137 infer env (App e1 e2)
139 >>= \tv-> infer env e1
140 >>= \(s1, t1)->infer (apply s1 env) e2
141 >>= \(s2, t2)->unify (apply s2 t1) (TFun t2 tv)
142 >>= \s3-> pure (compose (compose s3 s2) s1, apply s3 tv)
143 infer env (Lambda x b)
145 >>= \tv-> infer ('Data.Map'.put x (Forall [] tv) env) b
146 >>= \(s1, t1)->pure (s1, TFun (apply s1 tv) t1)
147 infer env (Builtin c a) = undef
148 infer env (Let x e1 e2)
150 >>= \(s1, t1)->let env` = apply s1 env in infer ('Data.Map'.put x (generalize env` t1) env) e2
151 >>= \(s2, t2)->pure (compose s1 s2, t2)