From: Mart Lubbers <mart@martlubbers.net>
Date: Wed, 18 Jul 2018 12:44:20 +0000 (+0200)
Subject: infer
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=81f620c2c7d7bbe1ce8b7e2a573bd643e6b22f5e;p=fp.git

infer
---

diff --git a/ast.dcl b/ast.dcl
index a24b2df..a490153 100644
--- a/ast.dcl
+++ b/ast.dcl
@@ -9,6 +9,7 @@ definition module ast
 	| Variable String
 	| Apply Expression Expression
 	| Lambda String Expression
+	| Let String Expression Expression
 	| Code String
 	| ..
 
diff --git a/ast.icl b/ast.icl
index 3f52921..8911114 100644
--- a/ast.icl
+++ b/ast.icl
@@ -15,7 +15,8 @@ where
 	pretty (Literal v) = pretty v
 	pretty (Variable v) = string v
 	pretty (Apply a b) = parens (pretty a <+> pretty b)
-	pretty (Lambda a b) = string "\\" <-> string a <-> string "->" <-> pretty b
+	pretty (Lambda a b) = string "\\" <-> string a <+> string "->" <+> pretty b
+	pretty (Let v a b) = string "let" <+> string v <+> string "=" <+> pretty a <+> string "in" <+> pretty b
 	pretty (Code b) = string "code" <+> string b
 
 instance Pretty Function
diff --git a/infer.dcl b/infer.dcl
new file mode 100644
index 0000000..1c1d294
--- /dev/null
+++ b/infer.dcl
@@ -0,0 +1,11 @@
+definition module infer
+
+from Data.Map import :: Map
+
+:: Type
+	= VarType String
+	| IntType
+	| BoolType
+	| CharType
+	| Arrow Type Type
+:: Scheme = Forall [String] Type
diff --git a/infer.icl b/infer.icl
new file mode 100644
index 0000000..fadc684
--- /dev/null
+++ b/infer.icl
@@ -0,0 +1,110 @@
+implementation module infer
+
+import StdEnv
+
+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.RWST
+
+import ast
+
+:: TypeEnv :== 'DM'.Map String Scheme
+:: Constraint :== (Type, Type)
+:: Subst :== 'DM'.Map String Type
+:: Unifier :== (Subst, [Constraint])
+:: Infer a :== RWST TypeEnv [Constraint] InferState (Either TypeError) a
+:: InferState = { count :: Int }
+:: Solve a :== 'MS'.StateT Unifier (Either TypeError) a
+:: TypeError = UnboundVariable String
+
+nullSubst :: Subst
+nullSubst = 'DM'.newMap
+
+uni :: Type Type -> Infer ()
+uni t1 t2 = tell [(t1, t2)]
+
+inEnv :: (String, Scheme) (Infer a) -> Infer a
+inEnv (x, sc) m = local (\e->'DM'.put x sc $ 'DM'.del x e) m
+
+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)
+
+lookupEnv :: String -> Infer Type
+lookupEnv x = asks ('DM'.get x)
+	>>= maybe (liftT $ Left $ UnboundVariable x) instantiate
+
+class Substitutable a
+where
+	apply :: Subst a -> a
+	ftv   :: a -> 'DS'.Set String
+
+instance Substitutable Type
+where
+	apply s t=:(VarType a) = maybe t id $ 'DM'.get a s
+	apply s (Arrow t1 t2)  = Arrow (apply s t1) (apply s t2)
+	apply _ t = t
+
+	ftv (VarType a)   = 'DS'.singleton a
+	ftv (Arrow t1 t2) = 'DS'.union (ftv t1) (ftv t2)
+	ftv t             = 'DS'.newSet
+
+instance Substitutable Scheme
+where
+	apply s (Forall as t)   = Forall as $ apply (foldr 'DM'.del s as) t
+	ftv (Forall as t) = 'DS'.difference (ftv t) ('DS'.fromList as)
+
+instance Substitutable [a] | Substitutable a
+where
+	apply s ls = map (apply s) ls
+	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
+
+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 ('DS'.toList $ 'DS'.difference (ftv t) (ftv env)) t
+
+infer :: Expression -> Infer Type
+infer (Literal v) = case v of
+	Int  _ = pure IntType
+	Bool _ = pure BoolType
+	Char _ = pure CharType
+infer (Variable s) = lookupEnv s
+infer (Apply e1 e2)
+	=        infer e1
+	>>= \t1->infer e2
+	>>= \t2->fresh
+	>>= \tv->uni t1 (Arrow t2 tv)
+	>>|      pure tv
+infer (Lambda s e)
+	=        fresh
+	>>= \tv->inEnv (s, Forall [] tv) (infer e)
+	>>= \t-> pure (Arrow tv t)
+infer (Let x e1 e2)
+	=        ask
+	>>= \en->infer e1
+	>>= \t1->inEnv (x, generalize en t1) (infer e2)
+infer (Code c) = fresh >>= \v->pure case c of
+	"add" = Arrow v (Arrow v v)
+	"sub" = Arrow v (Arrow v v)
+	"mul" = Arrow v (Arrow v v)
+	"div" = Arrow v (Arrow v v)
+	"and" = Arrow v (Arrow v BoolType)
+	"or"  = Arrow v (Arrow v BoolType)
diff --git a/parse.dcl b/parse.dcl
index 9ac10cd..e059278 100644
--- a/parse.dcl
+++ b/parse.dcl
@@ -9,5 +9,5 @@ from StdOverloaded import class zero
 
 instance zero ParseState
 
-lex :: [Char] -> [Token]
+lex   :: [Char] -> [Token]
 parse :: [Token] ParseState -> Either [String] AST
diff --git a/parse.icl b/parse.icl
index e5927bd..4359629 100644
--- a/parse.icl
+++ b/parse.icl
@@ -22,33 +22,39 @@ import Data.Tuple
 derive consName Token, Value
 
 :: Expression | DelayedParse [Token]
-
 :: Token
 	= IntToken Int    | BoolToken Bool | CharToken Char | IdentToken String
 	| InfixrToken     | InfixlToken    | SemiColonToken | OpenBraceToken
 	| CloseBraceToken | EqualsToken    | CodeToken      | LambdaToken
-	| ArrowToken
+	| ArrowToken      | LetToken       | InToken
+:: ParseState = {tokens :: [Token], infixers :: [Infix]}
+:: Infix = Infix String Fixity Int
+:: Fixity = InfixL | InfixR
+:: Parser a :== StateT ParseState (Either [String]) a
+
+instance < Infix where (<) (Infix _ _ s) (Infix _ _ t) = s < t
+instance zero ParseState where zero = {tokens=[],infixers=[]}
 
 lex :: [Char] -> [Token]
 lex cs = lex` cs
 where
-	lex` [] = []
-	lex` ['\n':cs] = lex` cs
-	lex` [c:cs]
-		| isSpace c = lex` cs
-	lex` [';':cs] = [SemiColonToken:lex` cs]
-	lex` ['=',c:cs]
-		| not (isIdent c) = [EqualsToken:lex` [c:cs]]
-	lex` ['(':cs] = [OpenBraceToken:lex` cs]
-	lex` [')':cs] = [CloseBraceToken:lex` cs]
-	lex` ['-','>':cs] = [ArrowToken:lex` cs]
-	lex` ['\\':cs] = [LambdaToken:lex` cs]
-	lex` ['\'',c,'\'':cs] = [CharToken c:lex` cs]
-	lex` ['T','r','u','e':cs] = [BoolToken True:lex` cs]
-	lex` ['c','o','d','e':cs] = [CodeToken:lex` cs]
-	lex` ['F','a','l','s','e':cs] = [BoolToken True:lex` cs]
-	lex` ['i','n','f','i','x','r':cs] = [InfixrToken:lex` cs]
-	lex` ['i','n','f','i','x','l':cs] = [InfixlToken:lex` cs]
+	lex` []                            = []
+	lex` ['\n':cs]                     = lex` cs
+	lex` [c:cs] | isSpace c            = lex` cs
+	lex` [';':cs]                      = [SemiColonToken:lex` cs]
+	lex` ['=',c:cs] | not (isIdent c)  = [EqualsToken:lex` [c:cs]]
+	lex` ['(':cs]                      = [OpenBraceToken:lex` cs]
+	lex` [')':cs]                      = [CloseBraceToken:lex` cs]
+	lex` ['->':cs]                     = [ArrowToken:lex` cs]
+	lex` ['\\':cs]                     = [LambdaToken:lex` cs]
+	lex` ['\'',c,'\'':cs]              = [CharToken c:lex` cs]
+	lex` ['let':cs]    | whiteOrEnd cs = [LetToken:lex` cs]
+	lex` ['in':cs]     | whiteOrEnd cs = [InToken:lex` cs]
+	lex` ['code':cs]   | whiteOrEnd cs = [CodeToken:lex` cs]
+	lex` ['False':cs]  | whiteOrEnd cs = [BoolToken True:lex` cs]
+	lex` ['True':cs]   | whiteOrEnd cs = [BoolToken True:lex` cs]
+	lex` ['infixr':cs] | whiteOrEnd cs = [InfixrToken:lex` cs]
+	lex` ['infixl':cs] | whiteOrEnd cs = [InfixlToken:lex` cs]
 	lex` ['-',c:cs]
 		| isDigit c
 			= case lex` [c:cs] of
@@ -66,21 +72,12 @@ where
 			= [IdentToken $ toString [c:i]:lex` cs]
 		= abort $ "Huh lexer failed on: " +++ toString (toInt c)
 
+whiteOrEnd [] = True
+whiteOrEnd [c:cs] = isSpace c
+
 isIdent c = isAlpha c || elem c ['\'`']
 isFunny = flip elem ['!@#$%^&*\|+-?/\'<>.:~=']
 
-:: ParseState =
-	{ tokens   :: [Token]
-	, infixers :: [Infix]
-	}
-:: Infix = Infix String Fixity Int
-instance < Infix where (<) (Infix _ _ s) (Infix _ _ t) = s < t
-:: Fixity = InfixL | InfixR
-
-:: Parser a :== StateT ParseState (Either [String]) a
-
-instance zero ParseState where zero = {tokens=[],infixers=[]}
-
 (<?>) infixl 1 :: a (StateT b (Either (c a)) d) -> StateT b (Either (c a)) d | Semigroup (c a) & Applicative c
 (<?>) err p = StateT $ first (flip mappend (pure err)) o runStateT p
 
@@ -131,6 +128,7 @@ where
 	parseBasic
 		//Bracketed
 		=   token OpenBraceToken *> parseBracketed <* token CloseBraceToken
+		<|> Let <$> (token LetToken *> parseIdent <* token EqualsToken) <*> (parseExpr <* token InToken) <*> parseExpr
 		<|> Literal <$> Int <$> parseInt
 		<|> Code <$> (token CodeToken *> parseIdent)
 		<|> flip (foldr Lambda) <$> (token LambdaToken *> some parseIdent <* token ArrowToken) <*> parseExpr
@@ -139,17 +137,14 @@ where
 	parseBracketed :: Parser Expression
 	parseBracketed
 		//Curried prefix infix
-		= (\e op->Apply (Apply fpflip op) e) <$> parseIfx <*> parseExpr
+		= (\op->Lambda "_v" o Apply (Apply op (Variable "v"))) <$> parseIfx <*> parseExpr
 		//Regular Prefix infix
 		<|> parseIfx
 		//Curried flipped prefix infix
-		<|> Apply <$> parseExpr <*> parseIfx
+		<|> (\e op->Lambda "_v" (Apply (Apply op e) (Variable "v"))) <$> parseExpr <*> parseIfx
 		//Parse regular expression
 		<|> parseExpr
 
-	fpflip :: Expression
-	fpflip = Lambda "x" $ Lambda "y" $ Lambda "z" $ Apply (Apply (Variable "x") (Variable "z")) (Variable "y")
-
 	parseWithIfx :: ([String] String -> Bool) -> Parser String
 	parseWithIfx f = gets (\s->[i\\Infix i _ _<-s.infixers]) >>= flip parseIf parseIdent o f
 
@@ -183,6 +178,8 @@ Start =
 	['id x = x;'] ++
 	['const x y = x;'] ++
 	['flip x y z = x z y;'] ++
+	['twice f = f . f;'] ++
+	['fix f x = let x = f x in x;'] ++
 	['. infixr 9 f g x = f $ g x;'] ++
 	['$ infixr 0 = id;'] ++
 	['& infixr 0 = flip $;'] ++
@@ -192,5 +189,6 @@ Start =
 	['/ infixr 7 = code div;'] ++
 	['&& infixl 3 = code and;'] ++
 	['|| infixl 2 = code or;'] ++
-	['ap = f . g $ x;']
+	['ap = (1 +);'] ++
+	['ap = (+ 1);']
 	) zero