From: Mart Lubbers Date: Thu, 19 Jul 2018 13:01:13 +0000 (+0200) Subject: inference from haskell writing X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=HEAD;p=fp.git inference from haskell writing --- diff --git a/infer.dcl b/infer.dcl index 1c1d294..c284a33 100644 --- a/infer.dcl +++ b/infer.dcl @@ -9,3 +9,5 @@ from Data.Map import :: Map | CharType | Arrow Type Type :: Scheme = Forall [String] Type + +infer :: Expression -> Infer Type diff --git a/infer.icl b/infer.icl index fadc684..a9a4108 100644 --- a/infer.icl +++ b/infer.icl @@ -10,14 +10,17 @@ import Data.Func 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.Monad.RWST +import Control.Monad.State => qualified gets, put, modify +import Control.Monad.RWST => qualified put import ast +derive gEq 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 -:: TypeError = UnboundVariable String +:: TypeError + = UnboundVariable String + | UnificationFail Type Type + | UnificationMismatch [Type] [Type] + | InfiniteType String Type nullSubst :: Subst nullSubst = 'DM'.newMap @@ -40,7 +47,7 @@ letters :: [String] 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) @@ -72,8 +79,12 @@ 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 @@ -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) + +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