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