start work on unification

diff --git a/src/Lambda/Type.hs b/src/Lambda/Type.hs
index 9ffdae7..e54dbe5 100644 (file)
--- a/src/Lambda/Type.hs
+++ b/src/Lambda/Type.hs
@@ -12,6 +12,8 @@
 module Lambda.Type
   ( -- * Types
     Type(..)
 module Lambda.Type
   ( -- * Types
     Type(..)

+    -- * Type inference
+  , algW

   ) where
 
 import Lambda.Term
   ) 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 
 
 
 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
 
 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
 
 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
 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
       unify a tv
       return b
     _ -> Left $ "cannot apply " ++ show tu ++ " to " ++ show tv

-  
-
-