remove unnecessary

[fp.git] / src / HM.hs

diff --git a/src/HM.hs b/src/HM.hs
index 18c1f30..8f6df2f 100644 (file)
--- a/src/HM.hs
+++ b/src/HM.hs
@@ -16,7 +16,6 @@ module HM
   , TypedTerm(..)
     -- * Type inference
   , algW
   , TypedTerm(..)
     -- * Type inference
   , algW

-  , runTI

   ) where
 
 import Control.Monad.Except
   ) where
 
 import Control.Monad.Except


@@ -77,6 +76,11 @@ instantiate (TSForAll v t) = do
   nv <- newVar
   instantiate $ substituteS (Map.singleton v nv) t
 
   nv <- newVar
   instantiate $ substituteS (Map.singleton v nv) t
 

+generalize :: TypeEnv -> Type -> TypeScheme
+generalize e t = foldr TSForAll (TScheme t) vars
+  where
+    vars = Set.toList $ freeVarsT t Set.\\ Set.unions (map freeVarsS $ Map.elems e)
+

 unify :: Type -> Type -> TI Substitution
 unify (TypeVar a) t = varBind a t
 unify t (TypeVar a) = varBind a t
 unify :: Type -> Type -> TI Substitution
 unify (TypeVar a) t = varBind a t
 unify t (TypeVar a) = varBind a t


@@ -104,8 +108,21 @@ ti e (NTTerm (Lam x y)) = do
   let e' = Map.insert x (TScheme tv) e
   (s, t) <-  ti e' y
   return (s, TypeFunction (substituteT s tv) t)
   let e' = Map.insert x (TScheme tv) e
   (s, t) <-  ti e' y
   return (s, TypeFunction (substituteT s tv) t)

-
-algW :: TypedTerm -> TI Type
-algW t = do
+ti e (NTTerm (App a b)) = do
+  tv <- newVar 
+  (s1, t1) <- ti e a
+  (s2, t2) <- ti (Map.map (substituteS s1) e) b
+  s3 <- unify (substituteT s2 t1) (TypeFunction t2 tv)
+  return (s3 `composeSub` s2 `composeSub` s1, substituteT s3 tv)
+ti e (NTTerm (Let x a b)) = do
+  (s1, t1) <- ti e a
+  let t' = generalize (Map.map (substituteS s1) e) t1
+      e' = Map.insert x t' e
+  (s2, t2) <- ti (Map.map (substituteS s1) e') b
+  return (s1 `composeSub` s2, t2)
+  
+ 
+algW :: TypedTerm -> Either String Type
+algW t = fst . runTI $ do

   (s, u) <- ti Map.empty t
   return $ substituteT s u
   (s, u) <- ti Map.empty t
   return $ substituteT s u