From: Tomas Musil <tomik.musil@gmail.com>
Date: Tue, 30 Dec 2014 19:04:39 +0000 (+0100)
Subject: start work on unification
X-Git-Url: http://git.tomasm.cz/fp.git/commitdiff_plain/7b1d09697fa612b0ccdf30062dce7c6f0d5f4eeb

start work on unification
---

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
-  
-
-