infer

diff --git a/ast.dcl b/ast.dcl
index a24b2df..a490153 100644 (file)
--- 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 (file)
--- 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 (file)
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 (file)
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 (file)
--- 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 (file)
--- 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