1 implementation module check
5 import Control.Monad => qualified join
6 import Control.Monad.State
7 import Control.Monad.Trans
11 import Data.Map => qualified put, union, difference, find, updateAt
21 check :: [Function] -> Either [String] (Expression, Scheme)
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 = (\x->(e, x)) <$> runInfer (infer preamble (makeExpression fs e))
29 // = pure (makeExpression fs e, undef)
30 ([Function _ _ _], _) = Left ["Start cannot have arguments"]
32 makeExpression :: [Function] Expression -> Expression
33 makeExpression fs start
34 = foldr mkExpr start $ scc [(l, vars e [])\\(l, e)<-nicefuns]
36 mkExpr :: [[Char]] -> (Expression -> Expression)
37 mkExpr scc = Let [(l, e)\\(l, e)<-nicefuns, s<-scc | s == l]
39 nicefuns :: [([Char], Expression)]
40 nicefuns = [(l, foldr ((o) o Lambda) id i e)\\(Function l i e)<-fs]
42 vars :: Expression [[Char]] -> [[Char]]
46 vars (App l r) c = vars l $ vars r c
47 vars (Lambda l e) c = [v\\v<-vars e c | v <> l]
48 vars (Let ns e) c = flatten
49 [ [v\\v<-vars e c | not (isMember v (map fst ns))]
50 : map (\(i, e)->[v\\v<-vars e [] | v <> i]) ns]
53 instance toString Scheme where
54 toString (Forall [] t) = toString t
55 toString (Forall as t) = concat ["A.", join " " (map toString as), ": ", toString t]
57 instance toString Type where
58 toString (TVar a) = toString a
60 toString TBool = "Bool"
61 toString (a --> b) = concat ["(", toString a, ") -> ", toString b]
63 :: TypeEnv :== Map [Char] Scheme
66 [(['_if'], Forall [['_ift']]
67 $ TBool --> TVar ['_ift'] --> TVar ['_ift'] --> TVar ['_ift'])
68 ,(['_eq'], Forall [['_eq']] $ TInt --> TInt --> TBool)
69 ,(['_mul'], Forall [['_mul']] $ TInt --> TInt --> TInt)
70 ,(['_add'], Forall [['_add']] $ TInt --> TInt --> TInt)
71 ,(['_sub'], Forall [['_sub']] $ TInt --> TInt --> TInt)
73 :: Subst :== Map [Char] Type
75 :: Infer a :== StateT [Int] (Either [String]) a
76 runInfer :: (Infer (Subst, Type)) -> Either [String] Scheme
77 runInfer i = uncurry ((o) (generalize newMap) o apply)
78 <$> evalStateT i [0..]
81 fresh = getState >>= \[s:ss]->put ss >>| pure (TVar (['v':[c\\c<-:toString s]]))
83 (oo) infixl 9 :: Subst Subst -> Subst
84 (oo) s1 s2 = 'Data.Map'.union (apply s1 <$> s2) s1
86 class Substitutable a where
90 instance Substitutable Type where
91 apply s t=:(TVar v) = fromMaybe t (get v s)
92 apply s (t1 --> t2) = apply s t1 --> apply s t2
96 ftv (t1 --> t2) = on union ftv t1 t2
99 instance Substitutable Scheme where
100 apply s (Forall as t) = Forall as $ apply (foldr del s as) t
101 ftv (Forall as t) = difference (ftv t) (removeDup as)
103 instance Substitutable TypeEnv where
104 apply s env = apply s <$> env
105 ftv env = ftv (elems env)
107 instance Substitutable [a] | Substitutable a where
108 apply s l = apply s <$> l
109 ftv t = foldr (union o ftv) [] t
111 occursCheck :: [Char] -> (a -> Bool) | Substitutable a
112 occursCheck a = isMember a o ftv
114 unify :: Type Type -> Infer Subst
115 unify (l --> r) (l` --> r`)
117 >>= \s1->on unify (apply s1) r r`
118 >>= \s2->pure (s1 oo s2)
119 unify (TVar a) (TVar t)
120 | a == t = pure newMap
122 | occursCheck a t = liftT (Left ["Infinite type: ", toString a, " to ", toString t])
123 = pure (singleton a t)
124 unify t (TVar a) = unify (TVar a) t
125 unify TInt TInt = pure newMap
126 unify TBool TBool = pure newMap
127 unify t1 t2 = liftT (Left ["Cannot unify: ", toString t1, " with ", toString t2])
129 instantiate :: Scheme -> Infer Type
130 instantiate (Forall as t)
131 = sequence [fresh\\_<-as]
132 >>= \as`->pure (apply (fromList $ zip2 as as`) t)
134 generalize :: TypeEnv Type -> Scheme
135 generalize env t = Forall (difference (ftv t) (ftv env)) t
137 infer :: TypeEnv Expression -> Infer (Subst, Type)
138 infer env (Lit (Int _)) = pure (newMap, TInt)
139 infer env (Lit (Bool _)) = pure (newMap, TBool)
140 infer env (Var x) = case get x env of
141 Nothing = liftT (Left ["Unbound variable: ", toString x])
142 Just s = (\x->(newMap, x)) <$> instantiate s
143 infer env (App e1 e2)
145 >>= \tv-> infer env e1
146 >>= \(s1, t1)->infer (apply s1 env) e2
147 >>= \(s2, t2)->unify (apply s2 t1) (t2 --> tv)
148 >>= \s3-> pure (s1 oo s2 oo s3, apply s3 tv)
149 infer env (Lambda x b)
151 >>= \tv-> infer ('Data.Map'.put x (Forall [] tv) env) b
152 >>= \(s1, t1)->pure (s1, apply s1 tv --> t1)
153 //infer env (Let [(x, e1)] e2)
155 // >>= \(s1, t1)->infer ('Data.Map'.put x (generalize (apply s1 env) t1) env) e2
156 // >>= \(s2, t2)->pure (s1 oo s2, t2)
157 infer env (Let [(x, e1)] e2)
159 >>= \tv-> let env` = 'Data.Map'.put x (Forall [] tv) env
161 >>= \(s1,t1)-> unify t1 tv
162 >>= \t->infer ('Data.Map'.put x (generalize (apply s1 env`) t1) env`) e2
163 >>= \(s2, t2)->pure (s1 oo s2, t2)
165 = liftT (Left ["Mutual recursion typechecking not implemented yet"])
166 //infer env (Let xs e2)
167 // # (ns, bs) = unzip xs
168 // = sequence [fresh\\_<-ns]
169 // >>= \tvs-> let env` = foldr (uncurry putenv) env (zip2 ns tvs)
170 // in unzip <$> sequence (map infer env`) bs
171 // >>= \(ss,ts)-> let s = foldr (oo) newMap ss
173 // >>= \t->infer ('Data.Map'.put x (generalize (apply s1 env`) t1) env`) e2
174 // >>= \(s2, t2)->pure (s1 oo s2, t2)
176 putenv :: [Char] -> (Type TypeEnv -> TypeEnv)
177 putenv k = 'Data.Map'.put k o Forall []
179 unifyl :: [Type] -> Infer Subst
180 unifyl [t1,t2:ts] = unify t1 t2 >>= \s->unifyl [t2:map (apply s) ts]
181 unifyl _ = pure newMap