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 a e) e fs
29 = case runInfer (infer 'Data.Map'.newMap e) of
32 = Left [printToString s]
33 ([Function _ _ _], _) = Left ["Start cannot have arguments"]
36 derive gPrint Scheme, Type
39 :: Scheme = Forall [[Char]] Type
40 :: TypeEnv :== 'Data.Map'.Map [Char] Scheme
41 :: Subst :== 'Data.Map'.Map [Char] Type
42 nullSubst = 'Data.Map'.newMap
44 :: Infer a :== StateT [Int] (Either [String]) a
45 runInfer :: (Infer (Subst, Type)) -> Either [String] Scheme
46 runInfer i = uncurry closeOver <$> evalStateT i [0..]
48 closeOver :: Subst Type -> Scheme
49 closeOver sub ty = normalize (generalize 'Data.Map'.newMap (apply sub ty))
51 normalize :: Scheme -> Scheme
53 // normalize (Forall ts body) = Forall (snd <$> ord) (normtype body)
55 // ord = zip2 (removeDup $ fv body) (fmap letters)
58 // fv (TFun a b) = fv a ++ fv b
61 // normtype (TFun a b) = TFun (normtype a) (normtype b)
62 // normtype (TCon a) = TCon a
63 // normtype (TVar a) =
64 // case lookup a ord of
66 // Nothing = Left ["type variable not in signature"]
69 fresh = getState >>= \[s:ss]->put ss >>| pure (TVar (['v':[c\\c<-:toString s]]))
71 compose :: Subst Subst -> Subst
72 compose s1 s2 = 'Data.Map'.union (apply s1 <$> s2) s1
74 class Substitutable a where
78 instance Substitutable Type where
79 apply s t=:(TVar v) = 'Data.Map'.findWithDefault t v s
80 apply s (TFun t1 t2) = on TFun (apply s) t1 t2
84 ftv (TFun t1 t2) = on union ftv t1 t2
87 instance Substitutable Scheme where
88 apply s (Forall as t) = Forall as $ apply (foldr 'Data.Map'.del s as) t
89 ftv (Forall as t) = difference (ftv t) (removeDup as)
91 instance Substitutable TypeEnv where
92 apply s env = apply s <$> env
93 ftv env = ftv ('Data.Map'.elems env)
95 instance Substitutable [a] | Substitutable a where
96 apply s l = apply s <$> l
97 ftv t = foldr (union o ftv) [] t
99 occursCheck :: [Char] -> (a -> Bool) | Substitutable a
100 occursCheck a = isMember a o ftv
102 unify :: Type Type -> Infer Subst
103 unify (TFun l r) (TFun l` r`)
105 >>= \s1->on unify (apply s1) r r`
106 >>= \s2->pure (compose s1 s2)
107 unify (TVar a) t = bind a t
108 unify t (TVar a) = bind a t
109 unify TInt TInt = pure nullSubst
110 unify TBool TBool = pure nullSubst
111 unify t1 t2 = liftT (Left ["Cannot unify: ", toString t1, " with ", toString t2])
113 bind :: [Char] Type -> Infer Subst
114 bind a (TVar t) | a == t = pure nullSubst
116 | occursCheck a t = liftT (Left ["Infinite type: ", toString a, " and ", toString t])
117 = pure ('Data.Map'.singleton a t)
119 instantiate :: Scheme -> Infer Type
120 instantiate (Forall as t)
121 = sequence [fresh\\_<-as]
122 >>= \as`->pure (apply ('Data.Map'.fromList $ zip2 as as`) t)
124 generalize :: TypeEnv Type -> Scheme
125 generalize env t = Forall (difference (ftv t) (ftv env)) t
127 infer :: TypeEnv Expression -> Infer (Subst, Type)
128 infer env (Lit (Int _)) = pure (nullSubst, TInt)
129 infer env (Lit (Bool _)) = pure (nullSubst, TBool)
130 infer env (Var x) = case 'Data.Map'.get x env of
131 Nothing = liftT (Left ["Unbound variable: ", toString x])
132 Just s = tuple nullSubst <$> instantiate s
133 infer env (App e1 e2)
135 >>= \tv-> infer env e1
136 >>= \(s1, t1)->infer (apply s1 env) e2
137 >>= \(s2, t2)->unify (apply s2 t1) (TFun t2 tv)
138 >>= \s3-> pure (compose (compose s3 s2) s1, apply s3 tv)
139 infer env (Lambda x b)
141 >>= \tv-> infer ('Data.Map'.put x (Forall [] tv) env) b
142 >>= \(s1, t1)->pure (s1, TFun (apply s1 tv) t1)
143 infer env (Builtin c a) = undef
144 infer env (Let i args e b) = undef