TypeChecker

gistfile1.txt

module TypeChecker where

type Vname = String

data Vexp = Var Vname
          | Lambda Vname Vexp
          | Ap Vexp Vexp
          | Let [Vname] [Vexp] Vexp
          | Letrec [Vname] [Vexp] Vexp

-- type TVname = String
data TypeExp = TVar TVname
             | TCons String [TypeExp]
             deriving (Eq,Show)

arrow :: TypeExp -> TypeExp -> TypeExp
arrow t1 t2 = TCons "arrow" [t1,t2]

int :: TypeExp
int = TCons "int" []

cross :: TypeExp -> TypeExp -> TypeExp
cross t1 t2 = TCons "cross" [t1,t2]

list :: TypeExp -> TypeExp
list t = TCons "list" [t]

tvars_in :: TypeExp -> [TVname]
tvars_in t = tvars_in' t []
  where
    tvars_in' (TVar x) l     = x:l
    tvars_in' (TCons _ ts) l = foldr tvars_in' l ts

type Subst = TVname -> TypeExp

sub_type :: Subst -> TypeExp -> TypeExp
sub_type phi (TVar tvn)     = phi tvn
sub_type phi (TCons tcn ts) = TCons tcn (map (sub_type phi) ts)

scomp :: Subst -> Subst -> Subst
scomp sub2 sub1 tvn = sub_type sub2 (sub1 tvn)

id_subst :: Subst
id_subst tvn = TVar tvn

delta :: TVname -> TypeExp -> Subst
delta tvn t tvn'
  | tvn == tvn' = t
  | otherwise   = TVar tvn'

extend :: Subst -> TVname -> TypeExp -> Maybe Subst
extend phi tvn t
  | t == TVar tvn         = Just phi
  | tvn `elem` tvars_in t = Nothing
  | otherwise             = Just $ delta tvn t `scomp` phi

unify :: Subst -> (TypeExp,TypeExp) -> Maybe Subst
unify phi (TVar tvn, t)
  | phitvn == TVar tvn  = extend phi tvn phit
  | otherwise           = unify phi (phitvn,phit)
  where
    phitvn = phi tvn
    phit   = sub_type phi t
unify phi (TCons tcn ts, TVar tvn) = unify phi (TVar tvn, TCons tcn ts)
unify phi (TCons tcn ts, TCons tcn' ts')
  | tcn == tcn' = unifyl phi (ts `zip` ts')
  | otherwise   = Nothing

unifyl :: Subst -> [(TypeExp,TypeExp)] -> Maybe Subst
unifyl phi eqns = foldr unify' (Just phi) eqns
  where
    unify' eqn (Just phix) = unify phix eqn
    unify' _   Nothing     = Nothing

data TypeScheme = Scheme [TVname] TypeExp

unknowns_scheme :: TypeScheme -> [TVname]
unknowns_scheme (Scheme scvs t) = tvars_in t `bar` scvs

bar :: Eq a => [a] -> [a] -> [a]
bar xs ys = [x | x <- xs, not (x `elem` ys)]

sub_scheme :: Subst -> TypeScheme -> TypeScheme
sub_scheme phi (Scheme scvs t) = Scheme scvs (sub_type (exclude phi scvs) t)

exclude :: Subst -> [TVname] -> TVname -> TypeExp
exclude phi scvs tvn
  | tvn `elem` scvs = TVar tvn
  | otherwise       = phi tvn

dom :: [(a,b)] -> [a]
dom = map fst

val :: Eq a => [(a,b)] -> a -> b
val al k = head [v | (k',v) <- al, k == k']

install :: [(a,b)] -> a -> b -> [(a,b)]
install al k v = (k,v):al

mg :: Eq a => [(a, b)] -> [b]
mg al = map (val al) (dom al)

type TypeEnv = [(Vname,TypeScheme)]

unknowns_te :: TypeEnv -> [TVname]
unknowns_te gamma = concat (map unknowns_scheme (mg gamma))

sub_te :: Subst -> TypeEnv -> TypeEnv
sub_te phi gamma = [(x, sub_scheme phi st) | (x, st) <- gamma]

next_name :: NameSupply -> TVname
next_name ns = ns

deplete :: NameSupply -> TVname
deplete (n:ns) = (n+2:ns)
deplete _ = error "deplete"

split :: NameSupply -> (NameSupply,NameSupply)
split ns = (0:ns,1:ns)

type TVname = [Int]
type NameSupply = TVname

name_sequences :: NameSupply -> [TVname]
name_sequences ns = next_name ns : name_sequences (deplete ns)

tc :: TypeEnv -> NameSupply -> Vexp -> Maybe (Subst, TypeExp)
tc gamma ns (Var x)          = tcvar    gamma ns x
tc gamma ns (Ap e1 e2)       = tcap     gamma ns e1 e2
tc gamma ns (Lambda x e)     = tclambda gamma ns x e
tc gamma ns (Let xs es e)    = tclet    gamma ns xs es e
tc gamma ns (Letrec xs es e) = tcletrec gamma ns xs es e

tcl :: TypeEnv -> NameSupply -> [Vexp] -> Maybe (Subst,[TypeExp])
tcl _     _  []     = Just (id_subst,[])
tcl gamma ns (e:es) = tcl1 gamma ns0 es (tc gamma ns1 e)
  where
    (ns0,ns1) = split ns

tcl1 :: TypeEnv -> NameSupply -> [Vexp] -> Maybe (Subst,TypeExp) -> Maybe (Subst,[TypeExp])
tcl1 _     _  _  Nothing = Nothing
tcl1 gamma ns es (Just (phi,t)) = tcl2 phi t (tcl gamma' ns es)
  where
    gamma' = sub_te phi gamma

tcl2 :: Subst -> TypeExp -> Maybe (Subst,[TypeExp]) -> Maybe (Subst,[TypeExp])
tcl2 _   _ Nothing = Nothing
tcl2 phi t (Just (psi,ts)) = Just (psi `scomp` phi, sub_type psi t : ts)

tcvar :: TypeEnv -> NameSupply -> Vname -> Maybe (Subst,TypeExp)
tcvar gamma ns x = Just (id_subst, newinstance ns scheme)
  where
    scheme = val gamma x

newinstance :: NameSupply -> TypeScheme -> TypeExp
newinstance ns (Scheme scvs t) = sub_type phi t
  where
    al = scvs `zip` name_sequences ns
    phi = al_to_subst al

al_to_subst :: [(TVname,TVname)] -> Subst
al_to_subst al tvn
  | tvn `elem` dom al = TVar (val al tvn)
  | otherwise         = TVar tvn

tcap :: TypeEnv -> NameSupply -> Vexp -> Vexp -> Maybe (Subst,TypeExp)
tcap gamma ns e1 e2 = tcap1 tvn (tcl gamma ns' [e1,e2])
  where
    tvn = next_name ns
    ns' = deplete ns

tcap1 :: TVname -> Maybe (Subst, [TypeExp]) -> Maybe (TVname -> TypeExp, TypeExp)
tcap1 _ Nothing = Nothing
tcap1 tvn (Just (phi,[t1,t2])) = tcap2 tvn (unify phi (t1,t2 `arrow` TVar tvn))
tcap1 _ _ = error "tcap1"

tcap2 :: t1 -> Maybe (t1 -> t) -> Maybe (t1 -> t, t)
tcap2 _    Nothing = Nothing
tcap2 tvn (Just phi) = Just (phi, phi tvn)

tclambda :: TypeEnv -> NameSupply -> Vname -> Vexp -> Maybe (Subst,TypeExp)
tclambda gamma ns x e = tclambda1 tvn (tc gamma' ns' e)
  where
    ns' = deplete ns
    gamma' = new_bvar (x,tvn) : gamma
    tvn = next_name ns

tclambda1 :: t -> Maybe (t -> TypeExp, TypeExp) -> Maybe (t -> TypeExp, TypeExp)
tclambda1 _   Nothing = Nothing
tclambda1 tvn (Just (phi,t)) = Just (phi, phi tvn `arrow` t)

new_bvar :: (t, TVname) -> (t, TypeScheme)
new_bvar (x,tvn) = (x, Scheme [] (TVar tvn))

tclet :: TypeEnv -> NameSupply -> [Vname] -> [Vexp] -> Vexp -> Maybe (Subst, TypeExp)
tclet gamma ns xs es e = tclet1 gamma ns0 xs e (tcl gamma ns1 es)
  where
    (ns0,ns1) = split ns

tclet1 :: TypeEnv -> NameSupply -> [Vname] -> Vexp -> Maybe (Subst, [TypeExp]) -> Maybe (Subst, TypeExp)
tclet1 _     _  _  _ Nothing = Nothing
tclet1 gamma ns xs e (Just (phi,ts)) = tclet2 phi (tc gamma'' ns1 e)
  where
    gamma'' = add_decls gamma' ns0 xs ts
    gamma'  = sub_te phi gamma
    (ns0,ns1) = split ns

tclet2 :: Subst -> Maybe (Subst, t) -> Maybe (Subst, t)
tclet2 _   Nothing = Nothing
tclet2 phi (Just (phi',t)) = Just (phi' `scomp` phi, t)

add_decls :: TypeEnv -> NameSupply -> [Vname] -> [TypeExp] -> TypeEnv
add_decls gamma ns xs ts = zip xs schemes ++ gamma
  where
    schemes = map (genbar unknowns ns) ts
    unknowns = unknowns_te gamma
    
genbar :: [TVname] -> NameSupply -> TypeExp -> TypeScheme
genbar unknowns ns t = Scheme (map snd al) t'
  where
    al = scvs `zip` name_sequences ns
    scvs = nodups (tvars_in t) `bar` unknowns
    t' = sub_type (al_to_subst al) t

nodups :: Eq a => [a] -> [a]
nodups ys = f [] ys
  where
    f acc [] = acc
    f acc (x:xs)
      | x `elem` acc = f acc xs
      | otherwise    = f (x:acc) xs

tcletrec :: TypeEnv -> NameSupply -> [Vname] -> [Vexp] -> Vexp -> Maybe (Subst,TypeExp)
tcletrec gamma ns xs es e = tcletrec1 gamma ns0 nbvs e (tcl (nbvs ++ gamma) ns1 es)
  where
    (ns0,ns') = split ns
    (ns1,ns2) = split ns'
    nbvs = new_bvars xs ns2

new_bvars :: [t] -> NameSupply -> [(t, TypeScheme)]
new_bvars xs ns = map new_bvar (xs `zip` name_sequences ns)

tcletrec1 :: TypeEnv -> NameSupply -> TypeEnv -> Vexp -> Maybe (Subst, [TypeExp]) -> Maybe (Subst, TypeExp)
tcletrec1 _     _  _    _ Nothing = Nothing
tcletrec1 gamma ns nbvs e (Just (phi,ts)) =
    tcletrec2 gamma' ns nbvs' e (unifyl phi (ts `zip` ts'))
  where    
    ts' = map old_bvar nbvs'
    nbvs' = sub_te phi nbvs
    gamma' = sub_te phi gamma
    
old_bvar :: (t, TypeScheme) -> TypeExp
old_bvar (_,Scheme [] t) = t
old_bvar _ = error "old_bvar"

tcletrec2 :: TypeEnv -> NameSupply -> TypeEnv -> Vexp -> Maybe Subst -> Maybe (Subst, TypeExp)
tcletrec2 _     _  _    _ Nothing = Nothing
tcletrec2 gamma ns nbvs e (Just phi) = tclet2 phi (tc gamma'' ns1 e)
  where
    ts = map old_bvar nbvs'
    nbvs' = sub_te phi nbvs
    gamma' = sub_te phi gamma
    gamma'' = add_decls gamma' ns0 (map fst nbvs) ts
    (ns0,ns1) = split ns

skk :: Vexp
skk = Let ["S","K"] [rhs_S,rhs_K] body
  where
    var_S = Var "S"
    var_K = Var "K"
    var_x = Var "x"
    var_y = Var "y"
    var_z = Var "z"
    body = Ap (Ap var_S var_K) var_K
    rhs_S = plambda ["x","y","z"] body_S
    rhs_K = plambda ["x","y"] body_K
    body_S = Ap (Ap var_x var_z) (Ap var_y var_z)
    body_K = var_x
    plambda vs e = foldr Lambda e vs