inference from haskell writing

diff --git a/infer.dcl b/infer.dcl
index 1c1d294..c284a33 100644 (file)
--- a/infer.dcl
+++ b/infer.dcl
@@ -9,3 +9,5 @@ from Data.Map import :: Map
        | CharType
        | Arrow Type Type
 :: Scheme = Forall [String] Type
        | CharType
        | Arrow Type Type
 :: Scheme = Forall [String] Type

+
+infer :: Expression -> Infer Type

diff --git a/infer.icl b/infer.icl
index fadc684..a9a4108 100644 (file)
--- a/infer.icl
+++ b/infer.icl
@@ -10,14 +10,17 @@ import Data.Func
 import Data.Either
 import Data.List
 import Data.Maybe
 import Data.Either
 import Data.List
 import Data.Maybe

+import Data.GenEq

 import Control.Applicative
 import Control.Monad
 import Control.Monad.Trans
 import qualified Control.Monad.State as MS
 import Control.Applicative
 import Control.Monad
 import Control.Monad.Trans
 import qualified Control.Monad.State as MS

-import Control.Monad.RWST
+import Control.Monad.State => qualified gets, put, modify
+import Control.Monad.RWST => qualified put

 
 import ast
 
 
 import ast
 

+derive gEq Type

 :: TypeEnv :== 'DM'.Map String Scheme
 :: Constraint :== (Type, Type)
 :: Subst :== 'DM'.Map String Type
 :: TypeEnv :== 'DM'.Map String Scheme
 :: Constraint :== (Type, Type)
 :: Subst :== 'DM'.Map String Type


@@ -25,7 +28,11 @@ import ast
 :: Infer a :== RWST TypeEnv [Constraint] InferState (Either TypeError) a
 :: InferState = { count :: Int }
 :: Solve a :== 'MS'.StateT Unifier (Either TypeError) a
 :: Infer a :== RWST TypeEnv [Constraint] InferState (Either TypeError) a
 :: InferState = { count :: Int }
 :: Solve a :== 'MS'.StateT Unifier (Either TypeError) a

-:: TypeError = UnboundVariable String
+:: TypeError
+       = UnboundVariable String
+       | UnificationFail Type Type
+       | UnificationMismatch [Type] [Type]
+       | InfiniteType String Type

 
 nullSubst :: Subst
 nullSubst = 'DM'.newMap
 
 nullSubst :: Subst
 nullSubst = 'DM'.newMap


@@ -40,7 +47,7 @@ letters :: [String]
 letters = map toString $ [1..] >>= flip replicateM ['a'..'z']
 
 fresh :: Infer Type
 letters = map toString $ [1..] >>= flip replicateM ['a'..'z']
 
 fresh :: Infer Type

-fresh = get >>= \s=:{count}->put {s & count=count + 1} >>| pure (VarType $ letters !! count)
+fresh = get >>= \s=:{count}->'Control.Monad.RWST'.put {s & count=count + 1} >>| pure (VarType $ letters !! count)

 
 lookupEnv :: String -> Infer Type
 lookupEnv x = asks ('DM'.get x)
 
 lookupEnv :: String -> Infer Type
 lookupEnv x = asks ('DM'.get x)


@@ -72,8 +79,12 @@ where
        ftv t = foldr ('DS'.union o ftv) 'DS'.newSet t
 
 instance Substitutable TypeEnv where
        ftv t = foldr ('DS'.union o ftv) 'DS'.newSet t
 
 instance Substitutable TypeEnv where

-  apply s env = fmap (apply s) env
-  ftv env = ftv $ 'DM'.elems env
+       apply s env = fmap (apply s) env
+       ftv env = ftv $ 'DM'.elems env
+
+instance Substitutable Constraint where
+       apply s (t1, t2) = (apply s t1, apply s t2)
+       ftv (t1, t2) = 'DS'.union (ftv t1) (ftv t2)

 
 instantiate ::  Scheme -> Infer Type
 instantiate (Forall as t) = mapM (const fresh) as
 
 instantiate ::  Scheme -> Infer Type
 instantiate (Forall as t) = mapM (const fresh) as


@@ -108,3 +119,37 @@ infer (Code c) = fresh >>= \v->pure case c of
        "div" = Arrow v (Arrow v v)
        "and" = Arrow v (Arrow v BoolType)
        "or"  = Arrow v (Arrow v BoolType)
        "div" = Arrow v (Arrow v v)
        "and" = Arrow v (Arrow v BoolType)
        "or"  = Arrow v (Arrow v BoolType)

+
+unifies :: Type Type -> Solve Unifier
+unifies t1 t2
+       | t1 === t2 = pure ('DM'.newMap, [])
+unifies (VarType v) t = tbind v t
+unifies t (VarType v) = tbind v t
+unifies (Arrow t1 t2) (Arrow t3 t4) = unifyMany [t1, t2] [t3, t4]
+unifies t1 t2 = liftT (Left (UnificationFail t1 t2))
+
+unifyMany :: [Type] [Type] -> Solve Unifier
+unifyMany [] [] = pure ('DM'.newMap, [])
+unifyMany [t1:ts1] [t2:ts2] = unifies t1 t2
+       >>= \(su1, cs1)->unifyMany (apply su1 ts1) (apply su1 ts2)
+       >>= \(su2, cs2)->pure (su2 `compose` su1, cs1 ++ cs2)
+unifyMany t1 t2 = liftT (Left (UnificationMismatch t1 t2))
+
+(`compose`) infix 1 :: Subst Subst -> Subst
+(`compose`) s1 s2 = 'DM'.union (apply s1 <$> s2) s1
+
+tbind ::  String Type -> Solve Unifier
+tbind a t
+       | t === VarType a = pure ('DM'.newMap, [])
+       | occursCheck a t = liftT $ Left $ InfiniteType a t
+       = pure $ ('DM'.singleton a t, [])
+
+occursCheck ::  String a -> Bool | Substitutable a
+occursCheck a t = 'DS'.member a $ ftv t
+
+solver :: Solve Subst
+solver = getState >>= \(su, cs)->case cs of
+       [] = pure su
+       [(t1, t2):cs0] = unifies t1 t2
+               >>= \(su1, cs1)->'MS'.put (su1 `compose` su, cs1 ++ (apply su1 cs0))
+               >>| solver