check.icl

   1 implementation module check
   2
   3 import StdEnv
   4
   5 import qualified Data.Map as DM
   6 from Data.Map import instance Functor (Map k)
   7 import qualified Data.Set as DS
   8 import Data.Functor
   9 import Data.Func
  10 import Data.Either
  11 import Data.List
  12 import Data.Maybe
  13 import Control.Applicative
  14 import Control.Monad
  15 import Control.Monad.Trans
  16 import qualified Control.Monad.State as MS
  17 import Control.Monad.State => qualified gets, put, modify
  18 import Control.Monad.RWST => qualified put
  19
  20 import ast
  21
  22 check :: AST -> Either [String] (AST, [([Char], Scheme)])
  23 check (AST fs) = pure (AST fs, [])/*case inferAST preamble fs of
  24         Left e = Left e
  25         Right s = Right (AST fs, 'DM'.toList s)
  26 where
  27         preamble = 'DM'.fromList
  28                 [(['if'], Forall [['a']] $ TFun TBool $ TFun (TVar ['a']) $ TFun (TVar ['a']) $ TVar ['a'])
  29                 ,(['eq'], Forall [] $ TFun TInt $ TFun TInt TBool)
  30                 ,(['mul'], Forall [] $ TFun TInt $ TFun TInt TInt)
  31                 ,(['div'], Forall [] $ TFun TInt $ TFun TInt TInt)
  32                 ,(['add'], Forall [] $ TFun TInt $ TFun TInt TInt)
  33                 ,(['sub'], Forall [] $ TFun TInt $ TFun TInt TInt)
  34                 ]
  35 */
  36
  37 :: TypeEnv    :== 'DM'.Map [Char] Scheme
  38 :: Constraint :== (Type, Type)
  39 :: Subst      :== 'DM'.Map [Char] Type
  40 :: Unifier    :== (Subst, [Constraint])
  41 :: Infer a    :== RWST TypeEnv [Constraint] InferState (Either [String]) a
  42 :: InferState =   { count :: Int }
  43 :: Scheme     =   Forall [[Char]] Type
  44 :: Solve a    :== StateT Unifier (Either [String]) a
  45
  46 nullSubst :: Subst
  47 nullSubst = 'DM'.newMap
  48
  49 uni :: Type Type -> Infer ()
  50 uni t1 t2 = tell [(t1, t2)]
  51
  52 inEnv :: ([Char], Scheme) (Infer a) -> Infer a
  53 inEnv (x, sc) m = local (\e->'DM'.put x sc $ 'DM'.del x e) m
  54
  55 letters :: [[Char]]
  56 letters = [1..] >>= flip replicateM ['a'..'z']
  57
  58 fresh :: Infer Type
  59 fresh = get >>= \s=:{count}->'Control.Monad.RWST'.put {s & count=count + 1} >>| pure (TVar $ letters !! count)
  60
  61 class Substitutable a
  62 where
  63         apply :: Subst a -> a
  64         ftv   :: a -> [[Char]]
  65
  66 instance Substitutable Type
  67 where
  68         apply s t=:(TVar a) = maybe t id $ 'DM'.get a s
  69         apply s (TFun t1 t2)  = TFun (apply s t1) (apply s t2)
  70         apply _ t = t
  71
  72         ftv (TVar a)     = [a]
  73         ftv (TFun t1 t2) = union (ftv t1) (ftv t2)
  74         ftv t            = []
  75
  76 instance Substitutable Scheme
  77 where
  78         apply s (Forall as t)   = Forall as $ apply (foldr 'DM'.del s as) t
  79         ftv (Forall as t) = difference (ftv t) as
  80
  81 instance Substitutable [a] | Substitutable a
  82 where
  83         apply s ls = map (apply s) ls
  84         ftv t = foldr (union o ftv) [] t
  85
  86 instance Substitutable TypeEnv where
  87         apply s env = fmap (apply s) env
  88         ftv env = ftv $ 'DM'.elems env
  89
  90 instance Substitutable Constraint where
  91         apply s (t1, t2) = (apply s t1, apply s t2)
  92         ftv (t1, t2) = union (ftv t1) (ftv t2)
  93
  94 instantiate ::  Scheme -> Infer Type
  95 instantiate (Forall as t) = mapM (const fresh) as
  96         >>= \as`->let s = 'DM'.fromList $ zip2 as as` in pure $ apply s t
  97
  98 generalize :: TypeEnv Type -> Scheme
  99 generalize env t = Forall (difference (ftv t) (ftv env)) t
 100
 101 //:: Expression
 102 //      = Lit Value
 103 //      | Var [Char]
 104 //      | App Expression Expression
 105 //      | Lambda [Char] Expression
 106 //      | Builtin [Char] [Expression]
 107 inferExpr :: TypeEnv Expression -> Either [String] Scheme
 108 inferExpr env ex = case runRWST (infer ex) env {count=0} of
 109         Left e = Left e
 110         Right (ty, st, cs) = case runStateT solver ('DM'.newMap, cs) of
 111                 Left e = Left e
 112                 Right (s, _) = Right (closeOver (apply s ty))
 113
 114 closeOver :: Type -> Scheme
 115 closeOver t = normalize (generalize 'DM'.newMap t)
 116
 117 normalize :: Scheme -> Scheme
 118 normalize t = t
 119
 120 inferAST :: TypeEnv [Function] -> Either [String] TypeEnv
 121 inferAST env [] = Right env
 122 inferAST env [Function name args body:rest] = case inferExpr env (foldr Lambda body args) of
 123         Left e = Left e
 124         Right ty = inferAST ('DM'.put name ty env) rest
 125
 126 inferFunc :: [Function] -> Infer ()
 127 inferFunc [] = pure ()
 128 inferFunc [Function name args body:rest]
 129         =      ask
 130         >>= \en->infer (foldr Lambda body args)
 131         >>= \t1->inEnv (name, generalize en t1) (inferFunc rest)
 132         >>= \_->pure ()
 133
 134 infer :: Expression -> Infer Type
 135 infer (Lit v) = case v of
 136         Int  _ = pure TInt
 137         Bool _ = pure TBool
 138 infer (Var s) = asks ('DM'.get s)
 139         >>= maybe (liftT $ Left ["Unbound variable " +++ toString s]) instantiate
 140 infer (App e1 e2)
 141         =        infer e1
 142         >>= \t1->infer e2
 143         >>= \t2->fresh
 144         >>= \tv->uni t1 (TFun t2 tv)
 145         >>|      pure tv
 146 infer (Lambda s e)
 147         =        fresh
 148         >>= \tv->inEnv (s, Forall [] tv) (infer e)
 149         >>= \t-> pure (TFun tv t)
 150 //infer (Let x e1 e2)
 151 //      =        ask
 152 //      >>= \en->infer e1
 153 //      >>= \t1->inEnv (x, generalize en t1) (infer e2)
 154
 155 unifies :: Type Type -> Solve Unifier
 156 unifies TInt TInt = pure ('DM'.newMap, [])
 157 unifies TBool TBool = pure ('DM'.newMap, [])
 158 unifies (TVar a) (TVar b)
 159         | a == b = pure ('DM'.newMap, [])
 160 unifies (TVar v) t = tbind v t
 161 unifies t (TVar v) = tbind v t
 162 unifies (TFun t1 t2) (TFun t3 t4) = unifyMany [t1, t2] [t3, t4]
 163 unifies t1 t2 = liftT $ Left ["Cannot unify " +++ toString t1 +++ " with " +++ toString t2]
 164
 165 unifyMany :: [Type] [Type] -> Solve Unifier
 166 unifyMany [] [] = pure ('DM'.newMap, [])
 167 unifyMany [t1:ts1] [t2:ts2] = unifies t1 t2
 168         >>= \(su1, cs1)->unifyMany (apply su1 ts1) (apply su1 ts2)
 169         >>= \(su2, cs2)->pure (su2 `compose` su1, cs1 ++ cs2)
 170 unifyMany t1 t2 = liftT $ Left ["Length difference in unifyMany"]
 171
 172 (`compose`) infix 1 :: Subst Subst -> Subst
 173 (`compose`) s1 s2 = 'DM'.union (apply s1 <$> s2) s1
 174
 175 tbind ::  [Char] Type -> Solve Unifier
 176 tbind a (TVar b)
 177         | a == b = pure ('DM'.newMap, [])
 178 tbind a t
 179         | occursCheck a t = liftT $ Left ["Infinite type " +++ toString a +++ toString t]
 180         = pure $ ('DM'.singleton a t, [])
 181
 182 occursCheck ::  [Char] a -> Bool | Substitutable a
 183 occursCheck a t = isMember a $ ftv t
 184
 185 solver :: Solve Subst
 186 solver = getState >>= \(su, cs)->case cs of
 187         [] = pure su
 188         [(t1, t2):cs0] = unifies t1 t2
 189                 >>= \(su1, cs1)->'MS'.put (su1 `compose` su, cs1 ++ (apply su1 cs0))
 190                 >>| solver