HM type inference

diff --git a/src/HM.hs b/src/HM.hs
index 18c1f30..9c4aa76 100644 (file)
--- a/src/HM.hs
+++ b/src/HM.hs
@@ -77,6 +77,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,7 +109,20 @@ 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)

-
+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 -> TI Type
 algW t = do
   (s, u) <- ti Map.empty t
 algW :: TypedTerm -> TI Type
 algW t = do
   (s, u) <- ti Map.empty t

diff --git a/src/HM/Parser.hs b/src/HM/Parser.hs
index 47c4649..54e1e6a 100644 (file)
--- a/src/HM/Parser.hs
+++ b/src/HM/Parser.hs
@@ -13,7 +13,7 @@
 
 module HM.Parser 
   ( tRead
 
 module HM.Parser 
   ( tRead

-  , parseTerm
+  , parseTypedTerm

   )  where
 
 import Data.Char (isAsciiLower, isAsciiUpper)
   )  where
 
 import Data.Char (isAsciiLower, isAsciiUpper)


@@ -46,7 +46,8 @@ instance Show Term where
 
 instance Show TypedTerm where
   show (NTTerm t) = show t
 
 instance Show TypedTerm where
   show (NTTerm t) = show t

-  show (TTerm t tp) = braced $ show t ++ " :: " ++ show tp 
+  show (TTerm (Var x) tp) = x ++ " :: " ++ show tp 
+  show (TTerm t tp) = braced (show t) ++ " :: " ++ show tp 

 
 instance Show Type where
   show (Primitive t) = t
 
 instance Show Type where
   show (Primitive t) = t


@@ -65,11 +66,13 @@ tRead s = case parseOnly (parseTypedTerm <* endOfInput) (T.pack s) of
 parseTerm :: Parser Term
 parseTerm = parseLet <|>
             parseApp <|>
 parseTerm :: Parser Term
 parseTerm = parseLet <|>
             parseApp <|>

+            parseBraces parseTerm <|>

             parseVar <|>
             parseLambda
 
 parseTermNoApp :: Parser Term
             parseVar <|>
             parseLambda
 
 parseTermNoApp :: Parser Term

-parseTermNoApp = parseLet <|>
+parseTermNoApp = parseBraces parseTerm <|>
+            parseLet <|>

             parseVar <|>
             parseLambda
 
             parseVar <|>
             parseLambda
 


@@ -82,13 +85,13 @@ parseTypeAndTerm p = do
 
 
 parseTypedTermNoApp :: Parser TypedTerm
 
 
 parseTypedTermNoApp :: Parser TypedTerm

-parseTypedTermNoApp = parseBraces parseTypedTerm <|>
-                      parseTypeAndTerm parseTermNoApp <|>
+parseTypedTermNoApp = parseTypeAndTerm parseTermNoApp <|>
+                      parseBraces parseTypedTerm <|>

                       (NTTerm <$> parseTermNoApp)
 
 parseTypedTerm :: Parser TypedTerm
                       (NTTerm <$> parseTermNoApp)
 
 parseTypedTerm :: Parser TypedTerm

-parseTypedTerm = parseBraces parseTypedTerm <|>
-                 parseTypeAndTerm parseTerm <|>
+parseTypedTerm = parseTypeAndTerm parseTerm <|>
+                 parseBraces parseTypedTerm <|>

                  (NTTerm <$> parseTerm)
 
 parseType :: Parser Type
                  (NTTerm <$> parseTerm)
 
 parseType :: Parser Type