From 7b1d09697fa612b0ccdf30062dce7c6f0d5f4eeb Mon Sep 17 00:00:00 2001
From: Tomas Musil <tomik.musil@gmail.com>
Date: Tue, 30 Dec 2014 20:04:39 +0100
Subject: [PATCH] start work on unification

---
 src/Lambda/Type.hs | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/src/Lambda/Type.hs b/src/Lambda/Type.hs
index 9ffdae7..e54dbe5 100644
--- a/src/Lambda/Type.hs
+++ b/src/Lambda/Type.hs
@@ -12,6 +12,8 @@
 module Lambda.Type
   ( -- * Types
     Type(..)
+    -- * Type inference
+  , algW
   ) where
 
 import Lambda.Term
@@ -24,21 +26,25 @@ data TypeScheme = TScheme Type | TSForAll TypeVarName TypeScheme deriving (Show)
 
 data HMTerm = HMTerm Term TypeScheme | HMLet VarName HMTerm HMTerm TypeScheme 
 
+type Substitution = TypeScheme -> TypeScheme
+
 fresh :: TypeVarName
 fresh = undefined
 
 substitute :: TypeScheme -> TypeVarName -> TypeScheme -> TypeScheme
 substitute = undefined
 
-unify :: TypeScheme -> TypeScheme -> Either String TypeScheme
-unify = undefined
+unify :: TypeScheme -> TypeScheme -> Either String Substitution
+unify (TScheme (Primitive a)) (TScheme (Primitive b)) | a == b = Right id
+unify (TScheme (TypeVar a)) (TScheme (TypeVar b)) | a == b = Right id
+unify a b = Left "cannot unify " ++ show a ++ " with " ++ show b
 
 algW :: HMTerm -> Either String TypeScheme
 algW (HMTerm (Var _) t) = Right t
 algW (HMTerm (Lambda x t) (TScheme p)) = do
   let v = TScheme (TypeVar fresh)
   np <- substitute v x t
-  return $ unify p np
+  unify p np
 algW (HMTerm (App u v) t) = do
   tu <- algW u
   tv <- algW v
@@ -47,6 +53,3 @@ algW (HMTerm (App u v) t) = do
       unify a tv
       return b
     _ -> Left $ "cannot apply " ++ show tu ++ " to " ++ show tv
-  
-
-
-- 
2.4.2