From afc027ed2ff6fdf1aba286c4b6501ee240e36183 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Tom=C3=A1=C5=A1=20Musil?= <tomik.musil@gmail.com>
Date: Tue, 25 Aug 2015 17:57:39 +0200
Subject: [PATCH] HM type inference

---
 src/HM.hs        | 20 +++++++++++++++++++-
 src/HM/Parser.hs | 17 ++++++++++-------
 2 files changed, 29 insertions(+), 8 deletions(-)

diff --git a/src/HM.hs b/src/HM.hs
index 18c1f30..9c4aa76 100644
--- 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
 
+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
@@ -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)
-
+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
diff --git a/src/HM/Parser.hs b/src/HM/Parser.hs
index 47c4649..54e1e6a 100644
--- a/src/HM/Parser.hs
+++ b/src/HM/Parser.hs
@@ -13,7 +13,7 @@
 
 module HM.Parser 
   ( tRead
-  , parseTerm
+  , parseTypedTerm
   )  where
 
 import Data.Char (isAsciiLower, isAsciiUpper)
@@ -46,7 +46,8 @@ instance Show Term where
 
 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
@@ -65,11 +66,13 @@ tRead s = case parseOnly (parseTypedTerm <* endOfInput) (T.pack s) of
 parseTerm :: Parser Term
 parseTerm = parseLet <|>
             parseApp <|>
+            parseBraces parseTerm <|>
             parseVar <|>
             parseLambda
 
 parseTermNoApp :: Parser Term
-parseTermNoApp = parseLet <|>
+parseTermNoApp = parseBraces parseTerm <|>
+            parseLet <|>
             parseVar <|>
             parseLambda
 
@@ -82,13 +85,13 @@ parseTypeAndTerm p = do
 
 
 parseTypedTermNoApp :: Parser TypedTerm
-parseTypedTermNoApp = parseBraces parseTypedTerm <|>
-                      parseTypeAndTerm parseTermNoApp <|>
+parseTypedTermNoApp = parseTypeAndTerm parseTermNoApp <|>
+                      parseBraces parseTypedTerm <|>
                       (NTTerm <$> parseTermNoApp)
 
 parseTypedTerm :: Parser TypedTerm
-parseTypedTerm = parseBraces parseTypedTerm <|>
-                 parseTypeAndTerm parseTerm <|>
+parseTypedTerm = parseTypeAndTerm parseTerm <|>
+                 parseBraces parseTypedTerm <|>
                  (NTTerm <$> parseTerm)
 
 parseType :: Parser Type
-- 
2.4.2