infer.icl

   1 implementation module infer
   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.RWST
  18
  19 import ast
  20
  21 :: TypeEnv :== 'DM'.Map String Scheme
  22 :: Constraint :== (Type, Type)
  23 :: Subst :== 'DM'.Map String Type
  24 :: Unifier :== (Subst, [Constraint])
  25 :: Infer a :== RWST TypeEnv [Constraint] InferState (Either TypeError) a
  26 :: InferState = { count :: Int }
  27 :: Solve a :== 'MS'.StateT Unifier (Either TypeError) a
  28 :: TypeError = UnboundVariable String
  29
  30 nullSubst :: Subst
  31 nullSubst = 'DM'.newMap
  32
  33 uni :: Type Type -> Infer ()
  34 uni t1 t2 = tell [(t1, t2)]
  35
  36 inEnv :: (String, Scheme) (Infer a) -> Infer a
  37 inEnv (x, sc) m = local (\e->'DM'.put x sc $ 'DM'.del x e) m
  38
  39 letters :: [String]
  40 letters = map toString $ [1..] >>= flip replicateM ['a'..'z']
  41
  42 fresh :: Infer Type
  43 fresh = get >>= \s=:{count}->put {s & count=count + 1} >>| pure (VarType $ letters !! count)
  44
  45 lookupEnv :: String -> Infer Type
  46 lookupEnv x = asks ('DM'.get x)
  47         >>= maybe (liftT $ Left $ UnboundVariable x) instantiate
  48
  49 class Substitutable a
  50 where
  51         apply :: Subst a -> a
  52         ftv   :: a -> 'DS'.Set String
  53
  54 instance Substitutable Type
  55 where
  56         apply s t=:(VarType a) = maybe t id $ 'DM'.get a s
  57         apply s (Arrow t1 t2)  = Arrow (apply s t1) (apply s t2)
  58         apply _ t = t
  59
  60         ftv (VarType a)   = 'DS'.singleton a
  61         ftv (Arrow t1 t2) = 'DS'.union (ftv t1) (ftv t2)
  62         ftv t             = 'DS'.newSet
  63
  64 instance Substitutable Scheme
  65 where
  66         apply s (Forall as t)   = Forall as $ apply (foldr 'DM'.del s as) t
  67         ftv (Forall as t) = 'DS'.difference (ftv t) ('DS'.fromList as)
  68
  69 instance Substitutable [a] | Substitutable a
  70 where
  71         apply s ls = map (apply s) ls
  72         ftv t = foldr ('DS'.union o ftv) 'DS'.newSet t
  73
  74 instance Substitutable TypeEnv where
  75   apply s env = fmap (apply s) env
  76   ftv env = ftv $ 'DM'.elems env
  77
  78 instantiate ::  Scheme -> Infer Type
  79 instantiate (Forall as t) = mapM (const fresh) as
  80         >>= \as`->let s = 'DM'.fromList $ zip2 as as` in pure $ apply s t
  81 generalize :: TypeEnv Type -> Scheme
  82 generalize env t = Forall ('DS'.toList $ 'DS'.difference (ftv t) (ftv env)) t
  83
  84 infer :: Expression -> Infer Type
  85 infer (Literal v) = case v of
  86         Int  _ = pure IntType
  87         Bool _ = pure BoolType
  88         Char _ = pure CharType
  89 infer (Variable s) = lookupEnv s
  90 infer (Apply e1 e2)
  91         =        infer e1
  92         >>= \t1->infer e2
  93         >>= \t2->fresh
  94         >>= \tv->uni t1 (Arrow t2 tv)
  95         >>|      pure tv
  96 infer (Lambda s e)
  97         =        fresh
  98         >>= \tv->inEnv (s, Forall [] tv) (infer e)
  99         >>= \t-> pure (Arrow tv t)
 100 infer (Let x e1 e2)
 101         =        ask
 102         >>= \en->infer e1
 103         >>= \t1->inEnv (x, generalize en t1) (infer e2)
 104 infer (Code c) = fresh >>= \v->pure case c of
 105         "add" = Arrow v (Arrow v v)
 106         "sub" = Arrow v (Arrow v v)
 107         "mul" = Arrow v (Arrow v v)
 108         "div" = Arrow v (Arrow v v)
 109         "and" = Arrow v (Arrow v BoolType)
 110         "or"  = Arrow v (Arrow v BoolType)