check.icl

   1 implementation module check
   2
   3 import StdEnv
   4
   5 import Data.Either
   6 import Data.List
   7 import Data.Functor
   8 import Data.Func
   9 import Data.Maybe
  10 import Data.Tuple
  11 import Control.Monad => qualified join
  12 import Control.Monad.Trans
  13 import Control.Monad.State
  14 import Text
  15
  16 import qualified Data.Map
  17 from Data.Map import :: Map(..), newMap, get, instance Functor (Map k)
  18
  19 import ast
  20
  21 check :: [Function] -> Either [String] Expression
  22 check fs
  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 (foldr ((o) o Lambda) id a e)) e fs
  29                         = case runInfer (infer newMap e) of
  30                                 Left e = Left e
  31                                 Right s = Left [toString s]
  32                 ([Function _ _ _], _) = Left ["Start cannot have arguments"]
  33
  34 instance toString Scheme where
  35         toString (Forall as t) = concat ["A.", join " " (map toString as), ": ", toString t]
  36
  37 instance toString Type where
  38         toString (TVar a) = toString a
  39         toString TInt = "Int"
  40         toString TBool = "Bool"
  41         toString (TFun a b) = concat ["(", toString a, ") -> ", toString b]
  42
  43 :: TypeEnv :== Map [Char] Scheme
  44 :: Subst   :== Map [Char] Type
  45
  46 :: Infer a :== StateT [Int] (Either [String]) a
  47 runInfer :: (Infer (Subst, Type)) -> Either [String] Scheme
  48 runInfer i = uncurry ((o) (generalize newMap) o apply)
  49         <$> evalStateT i [0..]
  50
  51 fresh :: Infer Type
  52 fresh = getState >>= \[s:ss]->put ss >>| pure (TVar (['v':[c\\c<-:toString s]]))
  53
  54 compose :: Subst Subst -> Subst
  55 compose s1 s2 = 'Data.Map'.union (apply s1 <$> s2) s1
  56
  57 class Substitutable a where
  58         apply :: Subst a -> a
  59         ftv :: a -> [[Char]]
  60
  61 instance Substitutable Type where
  62         apply s t=:(TVar v) = fromMaybe t (get v s)
  63         apply s (TFun t1 t2) = on TFun (apply s) t1 t2
  64         apply _ x = x
  65
  66         ftv (TVar v) = [v]
  67         ftv (TFun t1 t2) = on union ftv t1 t2
  68         ftv _ = []
  69
  70 instance Substitutable Scheme where
  71         apply s (Forall as t) = Forall as $ apply (foldr 'Data.Map'.del s as) t
  72         ftv (Forall as t) = difference (ftv t) (removeDup as)
  73
  74 instance Substitutable TypeEnv where
  75         apply s env = apply s <$> env
  76         ftv env = ftv ('Data.Map'.elems env)
  77
  78 instance Substitutable [a] | Substitutable a where
  79         apply s l = apply s <$>  l
  80         ftv t = foldr (union o ftv) [] t
  81
  82 occursCheck :: [Char] -> (a -> Bool) | Substitutable a
  83 occursCheck a = isMember a o ftv
  84
  85 unify :: Type Type -> Infer Subst
  86 unify (TFun l r) (TFun l` r`)
  87         =        unify l l`
  88         >>= \s1->on unify (apply s1) r r`
  89         >>= \s2->pure (compose s1 s2)
  90 unify (TVar a) t = bind a t
  91 unify t (TVar a) = bind a t
  92 unify TInt TInt = pure 'Data.Map'.newMap
  93 unify TBool TBool = pure 'Data.Map'.newMap
  94 unify t1 t2 = liftT (Left ["Cannot unify: ", toString t1, " with ", toString t2])
  95
  96 bind :: [Char] Type -> Infer Subst
  97 bind a (TVar t) | a == t = pure 'Data.Map'.newMap
  98 bind a t
  99         | occursCheck a t = liftT (Left ["Infinite type: ", toString a, " and ", toString t])
 100         = pure ('Data.Map'.singleton a t)
 101
 102 instantiate :: Scheme -> Infer Type
 103 instantiate (Forall as t)
 104         =         sequence [fresh\\_<-as]
 105         >>= \as`->pure (apply ('Data.Map'.fromList $ zip2 as as`) t)
 106
 107 generalize :: TypeEnv Type -> Scheme
 108 generalize env t = Forall (difference (ftv t) (ftv env)) t
 109
 110 infer :: TypeEnv Expression -> Infer (Subst, Type)
 111 infer env (Lit (Int _)) = pure ('Data.Map'.newMap, TInt)
 112 infer env (Lit (Bool _)) = pure ('Data.Map'.newMap, TBool)
 113 infer env (Var x) = case 'Data.Map'.get x env of
 114         Nothing = liftT (Left ["Unbound variable: ", toString x])
 115         Just s = tuple 'Data.Map'.newMap <$> instantiate s
 116 infer env (App e1 e2)
 117         =              fresh
 118         >>= \tv->      infer env e1
 119         >>= \(s1, t1)->infer (apply s1 env) e2
 120         >>= \(s2, t2)->unify (apply s2 t1) (TFun t2 tv)
 121         >>= \s3->      pure (compose (compose s3 s2) s1, apply s3 tv)
 122 infer env (Lambda x b)
 123         =              fresh
 124         >>= \tv->      infer ('Data.Map'.put x (Forall [] tv) env) b
 125         >>= \(s1, t1)->pure (s1, TFun (apply s1 tv) t1)
 126 infer env (Builtin c a) = undef
 127 infer env (Let x e1 e2)
 128         =              infer env e1
 129         >>= \(s1, t1)->let env` = apply s1 env in infer ('Data.Map'.put x (generalize env` t1) env) e2
 130         >>= \(s2, t2)->pure (compose s1 s2, t2)