From: Mart Lubbers <mart@martlubbers.net>
Date: Tue, 5 Mar 2019 13:10:25 +0000 (+0100)
Subject: infer
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=96374f717c8200b7687525910c666b285521d80e;p=minfp.git

infer
---

diff --git a/check.icl b/check.icl
index e332b59..7d02871 100644
--- a/check.icl
+++ b/check.icl
@@ -4,202 +4,141 @@ import StdEnv
 
 import Data.Either
 import Data.List
+import Data.Functor
+import Data.Func
+import Data.Maybe
+import Data.Tuple
 import Control.Monad
+import Control.Monad.Trans
+import Control.Monad.State
+
+import qualified Data.Map
+from Data.Map import instance Functor (Map k)
 
 import ast
 
+import StdDebug
 check :: [Function] -> Either [String] Expression
 check fs
 	# dups = filter (\x->length x > 1) (groupBy (\(Function i _ _) (Function j _ _)->i == j) fs)
 	| length dups > 0 = Left ["Duplicate functions: ":[toString n\\[(Function n _ _):_]<-dups]]
 	= case partition (\a->a=:(Function ['start'] _ _)) fs of
 		([], _) = Left ["No start function defined"]
-		([Function _ [] e], fs) = Right (foldr (\(Function i a e)->Let i a e) e fs)
+		([Function _ [] e], fs)
+			# e = foldr (\(Function i a e)->Let i a e) e fs
+			= case runInfer (infer 'Data.Map'.newMap e) of
+				Left e = Left e
+				Right s
+					= Left [printToString s]
 		([Function _ _ _], _) = Left ["Start cannot have arguments"]
 
-//import qualified Data.Map as DM
-//from Data.Map import instance Functor (Map k)
-//import qualified Data.Set as DS
-//import Data.Functor
-//import Data.Func
-//import Data.Either
-//import Data.List
-//import Data.Maybe
-//import Control.Applicative
-//import Control.Monad
-//import Control.Monad.Trans
-//import qualified Control.Monad.State as MS
-//import Control.Monad.State => qualified gets, put, modify
-//import Control.Monad.RWST => qualified put
-//
-//import ast
-//
-//check :: AST -> Either [String] (AST, [([Char], Scheme)])
-//check (AST fs) = pure (AST fs, [])/*case inferAST preamble fs of
-//	Left e = Left e
-//	Right s = Right (AST fs, 'DM'.toList s)
-//where
-//	preamble = 'DM'.fromList
-//		[(['if'], Forall [['a']] $ TFun TBool $ TFun (TVar ['a']) $ TFun (TVar ['a']) $ TVar ['a'])
-//		,(['eq'], Forall [] $ TFun TInt $ TFun TInt TBool)
-//		,(['mul'], Forall [] $ TFun TInt $ TFun TInt TInt)
-//		,(['div'], Forall [] $ TFun TInt $ TFun TInt TInt)
-//		,(['add'], Forall [] $ TFun TInt $ TFun TInt TInt)
-//		,(['sub'], Forall [] $ TFun TInt $ TFun TInt TInt)
-//		]
-//*/
-//
-//:: TypeEnv    :== 'DM'.Map [Char] Scheme
-//:: Constraint :== (Type, Type)
-//:: Subst      :== 'DM'.Map [Char] Type
-//:: Unifier    :== (Subst, [Constraint])
-//:: Infer a    :== RWST TypeEnv [Constraint] InferState (Either [String]) a
-//:: InferState =   { count :: Int }
-//:: Scheme     =   Forall [[Char]] Type
-//:: Solve a    :== StateT Unifier (Either [String]) a
-//
-//nullSubst :: Subst
-//nullSubst = 'DM'.newMap
-//
-//uni :: Type Type -> Infer ()
-//uni t1 t2 = tell [(t1, t2)]
-//
-//inEnv :: ([Char], Scheme) (Infer a) -> Infer a
-//inEnv (x, sc) m = local (\e->'DM'.put x sc $ 'DM'.del x e) m
-//
-//letters :: [[Char]]
-//letters = [1..] >>= flip replicateM ['a'..'z']
-//
-//fresh :: Infer Type
-//fresh = get >>= \s=:{count}->'Control.Monad.RWST'.put {s & count=count + 1} >>| pure (TVar $ letters !! count)
-//
-//class Substitutable a
-//where
-//	apply :: Subst a -> a
-//	ftv   :: a -> [[Char]]
-//
-//instance Substitutable Type
-//where
-//	apply s t=:(TVar a) = maybe t id $ 'DM'.get a s
-//	apply s (TFun t1 t2)  = TFun (apply s t1) (apply s t2)
-//	apply _ t = t
-//
-//	ftv (TVar a)     = [a]
-//	ftv (TFun t1 t2) = union (ftv t1) (ftv t2)
-//	ftv t            = []
-//
-//instance Substitutable Scheme
-//where
-//	apply s (Forall as t)   = Forall as $ apply (foldr 'DM'.del s as) t
-//	ftv (Forall as t) = difference (ftv t) as
-//
-//instance Substitutable [a] | Substitutable a
-//where
-//	apply s ls = map (apply s) ls
-//	ftv t = foldr (union o ftv) [] t
-//
-//instance Substitutable TypeEnv where
-//	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) = union (ftv t1) (ftv t2)
-//
-//instantiate ::  Scheme -> Infer Type
-//instantiate (Forall as t) = mapM (const fresh) as
-//	>>= \as`->let s = 'DM'.fromList $ zip2 as as` in pure $ apply s t
-//
-//generalize :: TypeEnv Type -> Scheme
-//generalize env t = Forall (difference (ftv t) (ftv env)) t
-//
-////:: Expression
-////	= Lit Value
-////	| Var [Char]
-////	| App Expression Expression
-////	| Lambda [Char] Expression
-////	| Builtin [Char] [Expression]
-//inferExpr :: TypeEnv Expression -> Either [String] Scheme
-//inferExpr env ex = case runRWST (infer ex) env {count=0} of
-//	Left e = Left e
-//	Right (ty, st, cs) = case runStateT solver ('DM'.newMap, cs) of
-//		Left e = Left e
-//		Right (s, _) = Right (closeOver (apply s ty))
-//
-//closeOver :: Type -> Scheme
-//closeOver t = normalize (generalize 'DM'.newMap t)
-//
-//normalize :: Scheme -> Scheme
-//normalize t = t 
-//
-//inferAST :: TypeEnv [Function] -> Either [String] TypeEnv
-//inferAST env [] = Right env
-//inferAST env [Function name args body:rest] = case inferExpr env (foldr Lambda body args) of
-//	Left e = Left e
-//	Right ty = inferAST ('DM'.put name ty env) rest
-//
-//inferFunc :: [Function] -> Infer ()
-//inferFunc [] = pure () 
-//inferFunc [Function name args body:rest]
-//	=      ask
-//	>>= \en->infer (foldr Lambda body args)
-//	>>= \t1->inEnv (name, generalize en t1) (inferFunc rest)
-//	>>= \_->pure ()
-//
-//infer :: Expression -> Infer Type
-//infer (Lit v) = case v of
-//	Int  _ = pure TInt
-//	Bool _ = pure TBool
-//infer (Var s) = asks ('DM'.get s)
-//	>>= maybe (liftT $ Left ["Unbound variable " +++ toString s]) instantiate
-//infer (App e1 e2)
-//	=        infer e1
-//	>>= \t1->infer e2
-//	>>= \t2->fresh
-//	>>= \tv->uni t1 (TFun t2 tv)
-//	>>|      pure tv
-//infer (Lambda s e)
-//	=        fresh
-//	>>= \tv->inEnv (s, Forall [] tv) (infer e)
-//	>>= \t-> pure (TFun tv t)
-////infer (Let x e1 e2)
-////	=        ask
-////	>>= \en->infer e1
-////	>>= \t1->inEnv (x, generalize en t1) (infer e2)
-//
-//unifies :: Type Type -> Solve Unifier
-//unifies TInt TInt = pure ('DM'.newMap, [])
-//unifies TBool TBool = pure ('DM'.newMap, [])
-//unifies (TVar a) (TVar b) 
-//	| a == b = pure ('DM'.newMap, [])
-//unifies (TVar v) t = tbind v t
-//unifies t (TVar v) = tbind v t
-//unifies (TFun t1 t2) (TFun t3 t4) = unifyMany [t1, t2] [t3, t4]
-//unifies t1 t2 = liftT $ Left ["Cannot unify " +++ toString t1 +++ " with " +++ toString 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 ["Length difference in unifyMany"]
-//
-//(`compose`) infix 1 :: Subst Subst -> Subst
-//(`compose`) s1 s2 = 'DM'.union (apply s1 <$> s2) s1
-//
-//tbind ::  [Char] Type -> Solve Unifier
-//tbind a (TVar b)
-//	| a == b = pure ('DM'.newMap, [])
-//tbind a t
-//	| occursCheck a t = liftT $ Left ["Infinite type " +++ toString a +++ toString t]
-//	= pure $ ('DM'.singleton a t, [])
-//
-//occursCheck ::  [Char] a -> Bool | Substitutable a
-//occursCheck a t = isMember 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
+import Text.GenPrint
+derive gPrint Scheme, Type
+
+//Polytypes
+:: Scheme = Forall [[Char]] Type
+:: TypeEnv :== 'Data.Map'.Map [Char] Scheme
+:: Subst   :== 'Data.Map'.Map [Char] Type
+nullSubst = 'Data.Map'.newMap
+
+:: Infer a :== StateT [Int] (Either [String]) a
+runInfer :: (Infer (Subst, Type)) -> Either [String] Scheme
+runInfer i = uncurry closeOver <$> evalStateT i [0..]
+where
+	closeOver :: Subst Type -> Scheme
+	closeOver sub ty = normalize (generalize 'Data.Map'.newMap (apply sub ty))
+
+	normalize :: Scheme -> Scheme
+	normalize i = i
+//	normalize (Forall ts body) = Forall (snd <$> ord) (normtype body)
+//	where
+//		ord = zip2 (removeDup $ fv body) (fmap letters)
+//
+//	fv (TVar a) = [a]
+//	fv (TFun a b) = fv a ++ fv b
+//	fv _ = []
+//
+//	normtype (TFun a b) = TFun (normtype a) (normtype b)
+//	normtype (TCon a)   = TCon a
+//	normtype (TVar a)   =
+//		  case lookup a ord of
+//			Just x = TVar x
+//			Nothing = Left ["type variable not in signature"]
+
+fresh :: Infer Type
+fresh = getState >>= \[s:ss]->put ss >>| pure (TVar (['v':[c\\c<-:toString s]]))
+
+compose :: Subst Subst -> Subst
+compose s1 s2 = 'Data.Map'.union (apply s1 <$> s2) s1
+
+class Substitutable a where
+	apply :: Subst a -> a
+	ftv :: a -> [[Char]]
+
+instance Substitutable Type where
+	apply s t=:(TVar v) = 'Data.Map'.findWithDefault t v s
+	apply s (TFun t1 t2) = on TFun (apply s) t1 t2
+	apply _ x = x
+	
+	ftv (TVar v) = [v]
+	ftv (TFun t1 t2) = on union ftv t1 t2
+	ftv _ = []
+
+instance Substitutable Scheme where
+	apply s (Forall as t) = Forall as $ apply (foldr 'Data.Map'.del s as) t
+	ftv (Forall as t) = difference (ftv t) (removeDup as)
+
+instance Substitutable TypeEnv where
+	apply s env = apply s <$> env
+	ftv env = ftv ('Data.Map'.elems env)
+
+instance Substitutable [a] | Substitutable a where
+	apply s l = apply s <$>  l
+	ftv t = foldr (union o ftv) [] t
+
+occursCheck :: [Char] -> (a -> Bool) | Substitutable a
+occursCheck a = isMember a o ftv
+
+unify :: Type Type -> Infer Subst
+unify (TFun l r) (TFun l` r`)
+	=        unify l l`
+	>>= \s1->on unify (apply s1) r r`
+	>>= \s2->pure (compose s1 s2)
+unify (TVar a) t = bind a t
+unify t (TVar a) = bind a t
+unify TInt TInt = pure nullSubst
+unify TBool TBool = pure nullSubst
+unify t1 t2 = liftT (Left ["Cannot unify: ", toString t1, " with ", toString t2])
+
+bind :: [Char] Type -> Infer Subst
+bind a (TVar t) | a == t = pure nullSubst
+bind a t
+	| occursCheck a t = liftT (Left ["Infinite type: ", toString a, " and ", toString t])
+	= pure ('Data.Map'.singleton a t)
+
+instantiate :: Scheme -> Infer Type
+instantiate (Forall as t)
+	=         sequence [fresh\\_<-as]
+	>>= \as`->pure (apply ('Data.Map'.fromList $ zip2 as as`) t)
+
+generalize :: TypeEnv Type -> Scheme
+generalize env t = Forall (difference (ftv t) (ftv env)) t
+
+infer :: TypeEnv Expression -> Infer (Subst, Type)
+infer env (Lit (Int _)) = pure (nullSubst, TInt)
+infer env (Lit (Bool _)) = pure (nullSubst, TBool)
+infer env (Var x) = case 'Data.Map'.get x env of
+	Nothing = liftT (Left ["Unbound variable: ", toString x])
+	Just s = tuple nullSubst <$> instantiate s
+infer env (App e1 e2)
+	=              fresh
+	>>= \tv->      infer env e1
+	>>= \(s1, t1)->infer (apply s1 env) e2
+	>>= \(s2, t2)->unify (apply s2 t1) (TFun t2 tv)
+	>>= \s3->      pure (compose (compose s3 s2) s1, apply s3 tv)
+infer env (Lambda x b)
+	=              fresh
+	>>= \tv->      infer ('Data.Map'.put x (Forall [] tv) env) b
+	>>= \(s1, t1)->pure (s1, TFun (apply s1 tv) t1)
+infer env (Builtin c a) = undef
+infer env (Let i args e b) = undef
diff --git a/parse.icl b/parse.icl
index 5bb4bac..7d4fb2e 100644
--- a/parse.icl
+++ b/parse.icl
@@ -67,7 +67,7 @@ pTop = getState >>= \s->case s.tokens of
 pEof :: Parser ()
 pEof = getState >>= \s->case s.tokens of
 	[] = pure ()
-	[t:ts] = liftT (Left ["Expected EOF"])
+	[t:ts] = liftT (Left ["Expected EOF but got ":map toString [t:ts]])
 
 (?) infixl 9 :: (Parser a) (a -> Bool) -> Parser a
 (?) p f = p >>= \v->if (f v) (pure v) empty
diff --git a/tests/preamble.mfp b/tests/preamble.mfp
index be7ee13..3263957 100644
--- a/tests/preamble.mfp
+++ b/tests/preamble.mfp
@@ -4,5 +4,5 @@ $ ifxr 0 x y = x y;
 * ifxl 7 x y = mul x y;
 - ifxl 6 x y = sub x y;
 + ifxl 6 x y = add x y;
-fac i = if (i == 0) 1 (i * fac (i - 1));
+fac i = if (i == 0) 1 $ i * fac (i - 1);
 start = fac 5;