, TypedTerm(..)
-- * Type inference
, algW
- , runTI
) where
import Control.Monad.Except
varBind :: TypeVarName -> Type -> TI Substitution
varBind v t | t == TypeVar v = return idSub
- | v `Set.member` freeVarsT t = fail $ "occur check failed: " ++ v ++ " in " ++ show t
+ | v `Set.member` freeVarsT t = fail $ "occur check failed: " ++ v ++ " ~ " ++ show t
| otherwise = return $ Map.singleton v t
instantiate :: TypeScheme -> TI Type
unify t (TypeVar a) = varBind a t
unify (TypeFunction a b) (TypeFunction a' b') = do
s1 <- unify a a'
- s2 <- unify b b'
+ s2 <- unify (substituteT s1 b) (substituteT s1 b')
return $ s1 `composeSub` s2
unify (Primitive a) (Primitive b) | a == b = return idSub
unify a b = fail $ "cannot unify " ++ show a ++ " with " ++ show b
+tiLit :: Literal -> TI (Substitution, Type)
+tiLit (LBool _) = return (idSub, Primitive "Bool")
+tiLit (LInt _) = return (idSub, Primitive "Integer")
+tiLit (LFunc If) = do
+ a <- newVar
+ return (idSub, Primitive "Bool" `TypeFunction` (a `TypeFunction` (a `TypeFunction` a)))
+
ti :: TypeEnv -> TypedTerm -> TI (Substitution, Type)
---ti _ (TTerm (Var v) (TScheme t@(Primitive _))) = return (idSub, t)
ti e (TTerm tr sch) = do
(s, t) <- ti e (NTTerm tr)
sch' <- instantiate sch
s' <- unify t sch'
return (s', substituteT s' sch')
+ti _ (NTTerm (Lit l)) = tiLit l
ti e (NTTerm (Var v)) = case Map.lookup v e of
Nothing -> fail $ "unbound variable: " ++ v
Just sigma -> do
e' = Map.insert x t' e
(s2, t2) <- ti (Map.map (substituteS s1) e') b
return (s1 `composeSub` s2, t2)
-
-algW :: TypedTerm -> TI Type
-algW t = do
+algW :: TypedTerm -> Either String Type
+algW t = fst . runTI $ do
(s, u) <- ti Map.empty t
return $ substituteT s u