check.icl

   1 implementation module check
   2
   3 import StdEnv
   4 import Data.Either
   5 import Data.List
   6 import Data.Functor
   7 import Data.Func
   8 import Data.Maybe
   9 import Data.Monoid
  10 import Control.Applicative
  11 import Control.Monad
  12 import Control.Monad.Trans
  13 import Control.Monad.RWST
  14 import qualified Data.Map as DM
  15 from Data.Map import instance Functor (Map k)
  16
  17 import ast
  18
  19 //Start = runRWST (infer (AST [(Function ['s','t','a','r','t'] [] (Lit (Int 42)))])
  20 Start = runRWST (infer (TypeEnv 'DM'.newMap) t) [] {tiSupply=0,tiSubst='DM'.newMap}
  21 where
  22         t = Function ['start'] [] (Lit (Int 42))
  23
  24 check :: AST -> Either [String] (Type, AST)
  25 check (AST fs) = case find (\f->f=:(Function ['start'] [] _)) fs of
  26         Nothing = Left ["No start function defined"]
  27         Just _ = Right undef/*case runRWST (infer fs) [] 'DM'.newMap of
  28                 Left e = Left e
  29                 Right (a, s, _) = Right (a, s)
  30 */
  31
  32 :: Type
  33         = TVar [Char]
  34         | TInt
  35         | TBool
  36         | TChar
  37         | TFun Type Type
  38
  39 instance == Type where
  40         (==) (TVar a) (TVar b) = a == b
  41         (==) TInt TInt = True
  42         (==) TBool TBool = True
  43         (==) TChar TChar = True
  44         (==) (TFun a1 a2) (TFun b1 b2) = a1 == b1 && a2 == b2
  45         (==) _ _ = False
  46
  47 instance toString Type where
  48         toString (TVar s) = toString s
  49         toString TInt = "Int"
  50         toString TBool = "Bool"
  51         toString TChar = "Char"
  52         toString (TFun t1 t2) = toString t1 +++ " -> " +++ toString t2
  53
  54 :: Scheme = Scheme [[Char]] Type
  55 class Types a where
  56         ftv :: a -> [[Char]]
  57         apply :: Subst a -> a
  58
  59 instance Types Type where
  60         ftv (TVar n) = [n]
  61         ftv TInt = []
  62         ftv TBool = []
  63         ftv TChar = []
  64         ftv (TFun t1 t2) = union (ftv t1) (ftv t2)
  65
  66         apply s (TVar n) = case 'DM'.get n s of
  67                 Nothing = TVar n
  68                 Just t = t
  69         apply s (TFun t1 t2) = TFun (apply s t1) (apply s t2)
  70         apply s t = t
  71
  72 instance Types Scheme where
  73         ftv (Scheme vars t) = difference (ftv t) vars
  74         apply s (Scheme vars t) = Scheme vars (apply (foldr 'DM'.del s vars) t)
  75
  76 instance Types [a] | Types a where
  77         ftv l = foldr union [] (map ftv l)
  78         apply s l = map (apply s) l
  79
  80 :: Subst :== 'DM'.Map [Char] Type
  81 composeSubst s1 s2 = 'DM'.union ((apply s1) <$> s2) s1
  82
  83 :: TypeEnv = TypeEnv ('DM'.Map [Char] Scheme)
  84 remove :: TypeEnv [Char] -> TypeEnv
  85 remove (TypeEnv env) var = TypeEnv ('DM'.del var env)
  86
  87 instance Types TypeEnv where
  88         ftv (TypeEnv env) = ftv ('DM'.elems env)
  89         apply s (TypeEnv env) = TypeEnv (apply s <$> env)
  90
  91 generalize :: TypeEnv Type -> Scheme
  92 generalize env t = Scheme (difference (ftv t) (ftv env)) t
  93
  94 :: TI a :== RWST TIEnv () TIState (Either [String]) a
  95 :: TIState = {tiSupply :: Int, tiSubst :: Subst}
  96 :: TIEnv :== [Int]
  97
  98 mgu :: Type Type -> TI Subst
  99 mgu (TFun l r) (TFun l` r`) = composeSubst <$> mgu l l` <*> mgu r r`
 100 mgu (TVar u) t = varBind u t
 101 mgu t (TVar u) = varBind u t
 102 mgu TInt TInt = pure 'DM'.newMap
 103 mgu TBool TBool = pure 'DM'.newMap
 104 mgu TChar TChar = pure 'DM'.newMap
 105 mgu t1 t2 = liftT (Left ["cannot unify: " +++ toString t1 +++ " with " +++ toString t2])
 106
 107 varBind :: [Char] Type -> TI Subst
 108 varBind u t
 109         | t == TVar u = pure 'DM'.newMap
 110         | isMember u (ftv t) = liftT (Left ["occur check fails: " +++ toString u +++ " vs. " +++ toString t])
 111         = pure ('DM'.singleton u t)
 112
 113 newTyVar :: [Char] -> TI Type
 114 newTyVar prefix
 115         =   get
 116         >>= \t->put {t & tiSupply=t.tiSupply+1}
 117         >>| pure (TVar (prefix ++ fromString (toString t.tiSupply)))
 118
 119 instantiate :: Scheme -> TI Type
 120 instantiate (Scheme vars t)
 121         = mapM (\_->newTyVar ['a']) vars
 122         >>= \nvars->pure (apply ('DM'.fromList (zip2 vars nvars)) t)
 123
 124 class infer a :: TypeEnv a -> TI (Subst, Type)
 125
 126 instance infer Value where
 127         infer _ (Int _) = pure ('DM'.newMap, TInt)
 128         infer _ (Bool _) = pure ('DM'.newMap, TBool)
 129         infer _ (Char _) = pure ('DM'.newMap, TChar)
 130
 131 instance infer Expression where
 132         infer e (Lit a) = infer e a
 133         infer (TypeEnv env) (Var v) = case 'DM'.get v env of
 134                 Nothing = liftT (Left ["unbound variable: " +++ toString v])
 135                 Just s = instantiate s >>= \t->pure ('DM'.newMap, t)
 136         infer env (App e1 e2)
 137                 =              newTyVar ['a']
 138                 >>= \tv      ->infer env e1
 139                 >>= \(s1, t1)->infer (apply s1 env) e2
 140                 >>= \(s2, t2)->mgu (apply s2 t1) (TFun t2 tv)
 141                 >>= \s3->pure (composeSubst s3 (composeSubst s2 s1), apply s3 tv)
 142         infer env (Lambda s e)
 143                 =        newTyVar ['l']
 144                 >>= \tv->
 145                         let (TypeEnv env`) = remove env s
 146                             env`` = TypeEnv ('DM'.union env` ('DM'.singleton s (Scheme [] tv)))
 147                         in infer env`` e
 148                 >>= \(s1, t1)->pure (s1, TFun (apply s1 tv) t1)
 149
 150 instance infer Function where
 151         infer env (Function name [] body)
 152                 = infer env body
 153
 154 typeInference :: ('DM'.Map [Char] Scheme) Expression -> TI Type
 155 typeInference env e = uncurry apply <$> infer (TypeEnv env) e