diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -6,7 +6,8 @@ **Mikrokosmos** is a λ-calculus interpreter, borrowing its name from the series of progressive piano études *[Mikrokosmos](https://www.youtube.com/watch?v=VEsMk3DAzWM)* written by *Bela Bartok*. -It aims to provide students with a tool to learn and understand lambda calculus. +It aims to provide students with a tool to learn and understand λ-calculus. It supports both untyped λ-calculus +and simply typed λ-calculus. * [Mikrokosmos user's guide](https://m42.github.io/mikrokosmos/). * [Mikrokosmos on Hackage](https://hackage.haskell.org/package/mikrokosmos). diff --git a/mikrokosmos.cabal b/mikrokosmos.cabal --- a/mikrokosmos.cabal +++ b/mikrokosmos.cabal @@ -1,5 +1,5 @@ name: mikrokosmos -version: 0.4.0 +version: 0.5.0 synopsis: Lambda calculus interpreter description: A didactic untyped lambda calculus interpreter. homepage: https://github.com/M42/mikrokosmos diff --git a/source/Format.hs b/source/Format.hs --- a/source/Format.hs +++ b/source/Format.hs @@ -152,4 +152,4 @@ -- | Version version :: String -version = "0.4.0" +version = "0.5.0" diff --git a/source/Interpreter.hs b/source/Interpreter.hs --- a/source/Interpreter.hs +++ b/source/Interpreter.hs @@ -66,8 +66,12 @@ env <- get let typed = getTypes env let illtyped = typed && typeinference (toBruijn (context env) le) == Nothing + let notypes = not typed && usestypecons (toBruijn (context env) le) - return $ if illtyped then [formatType ++ "Error: not typeable expression" ++ end ++ "\n"] else + return $ if illtyped then [formatType ++ "Error: non typeable expression" ++ end ++ "\n"] else + if notypes then [formatType ++ + "Error: this expression uses type constructors. You may want to activate ':types on'." + ++ end ++ "\n"] else [ unlines $ [ show le ] ++ [ unlines $ map showReduction $ simplifySteps $ toBruijn (context env) le ] ++ diff --git a/source/Lambda.hs b/source/Lambda.hs --- a/source/Lambda.hs +++ b/source/Lambda.hs @@ -10,10 +10,11 @@ -} module Lambda - ( Exp (Var, Lambda, App) + ( Exp (Var, Lambda, App, Pair, Pi1, Pi2, Inl, Inr, Caseof, Unit, Abort, Absurd) , simplifyAll , simplifySteps , showReduction + , usestypecons -- , freein ) where @@ -22,9 +23,18 @@ -- DeBruijn Expressions -- | A lambda expression using DeBruijn indexes. -data Exp = Var Integer -- ^ integer indexing the variable. - | Lambda Exp -- ^ lambda abstraction - | App Exp Exp -- ^ function application +data Exp = Var Integer -- ^ integer indexing the variable. + | Lambda Exp -- ^ lambda abstraction. + | App Exp Exp -- ^ function application. + | Pair Exp Exp -- ^ typed pair of expressions. + | Pi1 Exp -- ^ typed first projection. + | Pi2 Exp -- ^ typed second projection. + | Inl Exp -- ^ typed left injection. + | Inr Exp -- ^ typed right injection. + | Caseof Exp Exp Exp -- ^ typed case of. + | Unit -- ^ typed unit element. + | Abort Exp -- ^ typed abort derivation. + | Absurd Exp -- ^ typed absurd derivation. deriving (Eq, Ord) instance Show Exp where @@ -33,17 +43,26 @@ -- | Shows an expression with DeBruijn indexes. showexp :: Exp -> String -showexp (Var n) = show n -showexp (Lambda e) = "λ" ++ showexp e ++ "" -showexp (App f g) = "(" ++ showexp f ++ " " ++ showexp g ++ ")" +showexp (Var n) = show n +showexp (Lambda e) = "λ" ++ showexp e ++ "" +showexp (App f g) = "(" ++ showexp f ++ " " ++ showexp g ++ ")" +showexp (Pair a b) = "(" ++ showexp a ++ "," ++ showexp b ++ ")" +showexp (Pi1 m) = "(" ++ "fst " ++ showexp m ++ ")" +showexp (Pi2 m) = "(" ++ "snd " ++ showexp m ++ ")" +showexp (Inl m) = "(" ++ "inl " ++ showexp m ++ ")" +showexp (Inr m) = "(" ++ "inr " ++ showexp m ++ ")" +showexp (Caseof m n p) = "(" ++ "case " ++ showexp m ++ " of " ++ showexp n ++ "; " ++ showexp p ++ ")" +showexp (Unit) = "*" +showexp (Abort a) = "(abort " ++ showexp a ++ ")" +showexp (Absurd a) = "(absurd " ++ showexp a ++ ")" -- | Shows an expression coloring the next reduction. showReduction :: Exp -> String showReduction (Lambda e) = "λ" ++ showReduction e showReduction (App (Lambda f) x) = betaColor (App (Lambda f) x) showReduction (Var e) = show e -showReduction (App rs x) = "(" ++ showReduction rs ++ " " - ++ showReduction x ++ ")" +showReduction (App rs x) = "(" ++ showReduction rs ++ " " ++ showReduction x ++ ")" +showReduction e = show e -- | Colors a beta reduction betaColor :: Exp -> String @@ -56,14 +75,14 @@ ++ ")" betaColor e = show e --- | Colors all the appearances of a given color +-- | Colors all the appearances of a given index indexColor :: Integer -> Exp -> String indexColor n (Lambda e) = "λ" ++ indexColor (succ n) e indexColor n (App f g) = "(" ++ indexColor n f ++ " " ++ indexColor n g ++ ")" indexColor n (Var m) | n == m = formatSubs1 ++ show m ++ formatFormula | otherwise = show m - +indexColor _ e = show e @@ -91,13 +110,27 @@ where s = simplify e -- | Simplifies the expression recursively. --- Applies only a beta reduction at each step. +-- Applies only one parallel beta reduction at each step. simplify :: Exp -> Exp -simplify (Lambda e) = Lambda (simplify e) -simplify (App (Lambda f) x) = betared (App (Lambda f) x) -simplify (App (Var e) x) = App (Var e) (simplify x) -simplify (App (App f g) x) = App (simplify (App f g)) x -simplify (Var e) = Var e +simplify (Lambda e) = Lambda (simplify e) +simplify (App (Lambda f) x) = betared (App (Lambda f) x) +simplify (App (Var e) x) = App (Var e) (simplify x) +simplify (App (App f g) x) = App (simplify (App f g)) x +simplify (App a b) = App (simplify a) (simplify b) +simplify (Var e) = Var e +simplify (Pair a b) = Pair (simplify a) (simplify b) +simplify (Pi1 (Pair a _)) = a +simplify (Pi1 m) = Pi1 (simplify m) +simplify (Pi2 (Pair _ b)) = b +simplify (Pi2 m) = Pi2 (simplify m) +simplify (Inl m) = Inl (simplify m) +simplify (Inr m) = Inr (simplify m) +simplify (Caseof (Inl m) a _) = App a m +simplify (Caseof (Inr m) _ b) = App b m +simplify (Caseof a b c) = Caseof (simplify a) (simplify b) (simplify c) +simplify (Unit) = Unit +simplify (Abort a) = Abort (simplify a) +simplify (Absurd a) = Absurd (simplify a) -- | Applies beta-reduction to a function application. -- Leaves the rest of the operations untouched. @@ -112,6 +145,15 @@ -> Exp substitute n x (Lambda e) = Lambda (substitute (succ n) (incrementFreeVars 0 x) e) substitute n x (App f g) = App (substitute n x f) (substitute n x g) +substitute n x (Pair a b) = Pair (substitute n x a) (substitute n x b) +substitute n x (Pi1 a) = Pi1 (substitute n x a) +substitute n x (Pi2 a) = Pi2 (substitute n x a) +substitute n x (Inl a) = Inl (substitute n x a) +substitute n x (Inr a) = Inr (substitute n x a) +substitute n x (Caseof a b c) = Caseof (substitute n x a) (substitute n x b) (substitute n x c) +substitute _ _ (Unit) = Unit +substitute n x (Abort a) = Abort (substitute n x a) +substitute n x (Absurd a) = Absurd (substitute n x a) substitute n x (Var m) -- The lambda is replaced directly | n == m = x @@ -129,6 +171,15 @@ incrementFreeVars n (Var m) | m > n = Var (succ m) | otherwise = Var m +incrementFreeVars n (Pair a b) = Pair (incrementFreeVars n a) (incrementFreeVars n b) +incrementFreeVars n (Pi1 a) = Pi1 (incrementFreeVars n a) +incrementFreeVars n (Pi2 a) = Pi2 (incrementFreeVars n a) +incrementFreeVars n (Inl a) = Inl (incrementFreeVars n a) +incrementFreeVars n (Inr a) = Inr (incrementFreeVars n a) +incrementFreeVars n (Caseof a b c) = Caseof (incrementFreeVars n a) (incrementFreeVars n b) (incrementFreeVars n c) +incrementFreeVars _ (Unit) = Unit +incrementFreeVars n (Abort a) = Abort (incrementFreeVars n a) +incrementFreeVars n (Absurd a) = Absurd (incrementFreeVars n a) -- | Determines if the given variable is free on the expression. @@ -136,3 +187,9 @@ -- freein n (Var m) = n == m -- freein n (Lambda e) = freein (succ n) e -- freein n (App u v) = (freein n u) && (freein n v) + +usestypecons :: Exp -> Bool +usestypecons (Var _) = False +usestypecons (App a b) = usestypecons a || usestypecons b +usestypecons (Lambda b) = usestypecons b +usestypecons _ = True diff --git a/source/NamedLambda.hs b/source/NamedLambda.hs --- a/source/NamedLambda.hs +++ b/source/NamedLambda.hs @@ -8,7 +8,10 @@ -} module NamedLambda - ( NamedLambda (LambdaVariable, LambdaAbstraction, LambdaApplication) + ( NamedLambda (LambdaVariable, LambdaAbstraction, LambdaApplication, + TypedPair, TypedPi1, TypedPi2, + TypedInl, TypedInr, TypedCase, TypedUnit, TypedAbort, + TypedAbsurd) , lambdaexp , toBruijn , nameExp @@ -31,9 +34,18 @@ -- it into an internal representation. -- | A lambda expression with named variables. -data NamedLambda = LambdaVariable String -- ^ variable - | LambdaAbstraction String NamedLambda -- ^ lambda abstraction - | LambdaApplication NamedLambda NamedLambda -- ^ function application +data NamedLambda = LambdaVariable String -- ^ variable + | LambdaAbstraction String NamedLambda -- ^ lambda abstraction + | LambdaApplication NamedLambda NamedLambda -- ^ function application + | TypedPair NamedLambda NamedLambda -- ^ pair of expressions + | TypedPi1 NamedLambda -- ^ first projection + | TypedPi2 NamedLambda -- ^ second projection + | TypedInl NamedLambda -- ^ left injection + | TypedInr NamedLambda -- ^ right injection + | TypedCase NamedLambda NamedLambda NamedLambda -- ^ case of expressions + | TypedUnit -- ^ unit + | TypedAbort NamedLambda -- ^ abort + | TypedAbsurd NamedLambda -- ^ absurd -- | Parses a lambda expression with named variables. -- A lambda expression is a sequence of one or more autonomous @@ -51,7 +63,20 @@ -- at the top level. It can be a lambda abstraction, a variable or another -- potentially complex lambda expression enclosed in parentheses. simpleexp :: Parser NamedLambda -simpleexp = choice [lambdaAbstractionParser, variableParser, parens lambdaexp] +simpleexp = choice + [ try pairParser + , try pi1Parser + , try pi2Parser + , try inlParser + , try inrParser + , try caseParser + , try unitParser + , try abortParser + , try absurdParser + , try lambdaAbstractionParser + , try variableParser + , try (parens lambdaexp) + ] -- | The returned parser parenthesizes the given parser parens :: Parser a -> Parser a @@ -74,12 +99,48 @@ lambdaChar :: Char lambdaChar = '\\' +pairParser :: Parser NamedLambda +pairParser = parens (TypedPair <$> lambdaexp <*> (char ',' >> lambdaexp)) + +pi1Parser :: Parser NamedLambda +pi1Parser = TypedPi1 <$> (string "FST " >> lambdaexp) + +pi2Parser :: Parser NamedLambda +pi2Parser = TypedPi2 <$> (string "SND " >> lambdaexp) + +inlParser :: Parser NamedLambda +inlParser = TypedInl <$> (string "INL " >> lambdaexp) + +inrParser :: Parser NamedLambda +inrParser = TypedInr <$> (string "INR " >> lambdaexp) + +caseParser :: Parser NamedLambda +caseParser = TypedCase <$> (string "CASE " >> simpleexp) <*> (string " OF " >> simpleexp) <*> (string ";" >> simpleexp) + +unitParser :: Parser NamedLambda +unitParser = string "UNIT" >> return TypedUnit + +abortParser :: Parser NamedLambda +abortParser = TypedAbort <$> (string "ABORT " >> lambdaexp) + +absurdParser :: Parser NamedLambda +absurdParser = TypedAbsurd <$> (string "ABSURD " >> lambdaexp) + -- | Shows a lambda expression with named variables. -- Parentheses are ignored; they are written only around applications. showNamedLambda :: NamedLambda -> String showNamedLambda (LambdaVariable c) = c showNamedLambda (LambdaAbstraction c e) = "λ" ++ c ++ "." ++ showNamedLambda e ++ "" showNamedLambda (LambdaApplication f g) = "(" ++ showNamedLambda f ++ " " ++ showNamedLambda g ++ ")" +showNamedLambda (TypedPair a b) = "(" ++ showNamedLambda a ++ "," ++ showNamedLambda b ++ ")" +showNamedLambda (TypedPi1 a) = "(" ++ "FST " ++ showNamedLambda a ++ ")" +showNamedLambda (TypedPi2 a) = "(" ++ "SND " ++ showNamedLambda a ++ ")" +showNamedLambda (TypedInl a) = "(" ++ "INL " ++ showNamedLambda a ++ ")" +showNamedLambda (TypedInr a) = "(" ++ "INR " ++ showNamedLambda a ++ ")" +showNamedLambda (TypedCase a b c) = "(" ++ "CASE " ++ showNamedLambda a ++ " of " ++ showNamedLambda b ++ "; " ++ showNamedLambda c ++ ")" +showNamedLambda (TypedUnit) = "UNIT" +showNamedLambda (TypedAbort a) = "(" ++ "ABORT " ++ showNamedLambda a ++ ")" +showNamedLambda (TypedAbsurd a) = "(" ++ "ABSURD " ++ showNamedLambda a ++ ")" instance Show NamedLambda where show = showNamedLambda @@ -105,6 +166,15 @@ case Map.lookup c d of Just n -> Var n Nothing -> fromMaybe (Var 0) (MultiBimap.lookupR c context) +tobruijn d context (TypedPair a b) = Pair (tobruijn d context a) (tobruijn d context b) +tobruijn d context (TypedPi1 a) = Pi1 (tobruijn d context a) +tobruijn d context (TypedPi2 a) = Pi2 (tobruijn d context a) +tobruijn d context (TypedInl a) = Inl (tobruijn d context a) +tobruijn d context (TypedInr a) = Inr (tobruijn d context a) +tobruijn d context (TypedCase a b c) = Caseof (tobruijn d context a) (tobruijn d context b) (tobruijn d context c) +tobruijn _ _ (TypedUnit) = Unit +tobruijn d context (TypedAbort a) = Abort (tobruijn d context a) +tobruijn d context (TypedAbsurd a) = Absurd (tobruijn d context a) -- | Transforms a lambda expression with named variables to a deBruijn index expression. -- Uses only the dictionary of the variables in the current context. @@ -118,10 +188,20 @@ -- | Translates a deBruijn expression into a lambda expression -- with named variables, given a list of used and unused variable names. nameIndexes :: [String] -> [String] -> Exp -> NamedLambda -nameIndexes _ _ (Var 0) = LambdaVariable "undefined" -nameIndexes used _ (Var n) = LambdaVariable (used !! pred (fromInteger n)) -nameIndexes used new (Lambda e) = LambdaAbstraction (head new) (nameIndexes (head new:used) (tail new) e) -nameIndexes used new (App f g) = LambdaApplication (nameIndexes used new f) (nameIndexes used new g) +nameIndexes _ _ (Var 0) = LambdaVariable "undefined" +nameIndexes used _ (Var n) = LambdaVariable (used !! pred (fromInteger n)) +nameIndexes used new (Lambda e) = LambdaAbstraction (head new) (nameIndexes (head new:used) (tail new) e) +nameIndexes used new (App f g) = LambdaApplication (nameIndexes used new f) (nameIndexes used new g) +nameIndexes used new (Pair a b) = TypedPair (nameIndexes used new a) (nameIndexes used new b) +nameIndexes used new (Pi1 a) = TypedPi1 (nameIndexes used new a) +nameIndexes used new (Pi2 a) = TypedPi2 (nameIndexes used new a) +nameIndexes used new (Inl a) = TypedInl (nameIndexes used new a) +nameIndexes used new (Inr a) = TypedInr (nameIndexes used new a) +nameIndexes used new (Caseof a b c) = TypedCase (nameIndexes used new a) (nameIndexes used new b) (nameIndexes used new c) +nameIndexes _ _ (Unit) = TypedUnit +nameIndexes used new (Abort a) = TypedAbort (nameIndexes used new a) +nameIndexes used new (Absurd a) = TypedAbsurd (nameIndexes used new a) + -- | Gives names to every variable in a deBruijn expression using -- alphabetic order. diff --git a/source/Ski.hs b/source/Ski.hs --- a/source/Ski.hs +++ b/source/Ski.hs @@ -18,6 +18,15 @@ -- | A SKI combinator expression data Ski = S | K | I | Comb Ski Ski | Cte String + | Spair + | Spi1 + | Spi2 + | Sinl + | Sinr + | Scase + | Sunit + | Sabort + | Sabsurd deriving (Eq, Ord) instance Show Ski where @@ -34,8 +43,16 @@ showski (Comb x I) = showski x ++ showski I showski (Comb x (Cte c)) = showski x ++ showski (Cte c) showski (Comb x (Comb u v)) = showski x ++ "(" ++ showski (Comb u v) ++ ")" - - +showski (Comb x a) = showski x ++ showski a +showski (Spair) = "[PAIR]" +showski (Spi1) = "[FST]" +showski (Spi2) = "[SND]" +showski (Sinl) = "[INL]" +showski (Sinr) = "[INR]" +showski (Scase) = "[CASEOF]" +showski (Sunit) = "[UNIT]" +showski (Sabort) = "[ABORT]" +showski (Sabsurd) = "[ABSURD]" -- | SKI abstraction of a named lambda term. From a lambda expression -- creates a SKI equivalent expression. The following algorithm is a @@ -44,13 +61,20 @@ skiabs (LambdaVariable x) = Cte x skiabs (LambdaApplication m n) = Comb (skiabs m) (skiabs n) skiabs (LambdaAbstraction x m) = bracketabs x (skiabs m) +skiabs (TypedPair a b) = Comb (Comb Spair (skiabs a)) (skiabs b) +skiabs (TypedPi1 a) = Comb Spi1 (skiabs a) +skiabs (TypedPi2 a) = Comb Spi2 (skiabs a) +skiabs (TypedInl a) = Comb Sinl (skiabs a) +skiabs (TypedInr a) = Comb Sinr (skiabs a) +skiabs (TypedCase a b c) = Comb (Comb (Comb Scase (skiabs a)) (skiabs b)) (skiabs c) +skiabs (TypedUnit) = Sunit +skiabs (TypedAbort a) = Comb Sabort (skiabs a) +skiabs (TypedAbsurd a) = Comb Sabsurd (skiabs a) + -- | Bracket abstraction of a SKI term, as defined in Hindley-Seldin -- (2.18). bracketabs :: String -> Ski -> Ski -bracketabs _ S = Comb K S -bracketabs _ K = Comb K K -bracketabs _ I = Comb K I bracketabs x (Cte y) = if x == y then I else Comb K (Cte y) bracketabs x (Comb u (Cte y)) | freein x u && x == y = u @@ -59,40 +83,10 @@ bracketabs x (Comb u v) | freein x (Comb u v) = Comb K (Comb u v) | otherwise = Comb (Comb S (bracketabs x u)) (bracketabs x v) +bracketabs _ a = Comb K a -- | Checks if a given variable is used on a SKI expression. freein :: String -> Ski -> Bool -freein _ S = True -freein _ K = True -freein _ I = True freein x (Cte y) = not (x == y) freein x (Comb u v) = freein x u && freein x v - - --- -- | Bracket abstraction of a lambda term. The following algorithm is --- -- an adaptation to deBruijn indexes of the definition 2.18 and 9.10 --- -- of the Hindley-Seldin book. --- skiabs :: Exp -> Ski - --- -- Error, the formula is not a closed one --- skiabs (Var n) = undefined - --- -- The first case is the identity --- skiabs (Lambda (Var 1)) = I - --- -- Only if the variable is free --- skiabs (Lambda (App u (Var 1))) --- | freein 1 u = skiabs u --- | otherwise = Comb (Comb S (skiabs u)) I - --- -- Combination --- skiabs (Lambda m@(App u v)) --- | freein 1 m = Comb K (skiabs m) --- | otherwise = Comb (Comb S (skiabs u)) (skiabs v) - --- -- Error on pattern matching --- skiabs (Lambda e) = undefined - --- skiabs (App u v) = Comb (skiabs u) (skiabs v) - - +freein _ _ = True diff --git a/source/Types.hs b/source/Types.hs --- a/source/Types.hs +++ b/source/Types.hs @@ -24,17 +24,28 @@ -- | A type template is a free type variable or an arrow between two -- types; that is, the function type. -data Type = Tvar Variable | Arrow Type Type +data Type = Tvar Variable + | Arrow Type Type + | Times Type Type + | Union Type Type + | Unitty + | Bottom deriving (Eq) instance Show Type where - show (Tvar t) = typevariableNames !! (fromInteger t) - show (Arrow (Tvar x) (Tvar y)) = show (Tvar x) ++ " -> " ++ show (Tvar y) - show (Arrow (Tvar x) b ) = show (Tvar x) ++ " -> " ++ show b - show (Arrow a (Tvar y)) = "(" ++ show a ++ ") -> " ++ show (Tvar y) - show (Arrow a b ) = "(" ++ show a ++ ") -> " ++ show b - + show (Tvar t) = typevariableNames !! (fromInteger t) + show (Arrow a b) = showparens a ++ " → " ++ show b + show (Times a b) = showparens a ++ " × " ++ showparens b + show (Union a b) = showparens a ++ " + " ++ showparens b + show (Unitty) = "⊤" + show (Bottom) = "⊥" +showparens :: Type -> String +showparens (Tvar t) = show (Tvar t) +showparens Unitty = show Unitty +showparens Bottom = show Bottom +showparens m = "(" ++ show m ++ ")" + -- | Creates the substitution given by the change of a variable for -- the given type. subs :: Variable -> Type -> Substitution @@ -42,11 +53,19 @@ | x == y = typ | otherwise = Tvar y subs x typ (Arrow a b) = Arrow (subs x typ a) (subs x typ b) +subs x typ (Times a b) = Times (subs x typ a) (subs x typ b) +subs x typ (Union a b) = Union (subs x typ a) (subs x typ b) +subs _ _ Unitty = Unitty +subs _ _ Bottom = Bottom -- | Returns true if the given variable appears on the type. occurs :: Variable -> Type -> Bool occurs x (Tvar y) = x == y occurs x (Arrow a b) = occurs x a || occurs x b +occurs x (Times a b) = occurs x a || occurs x b +occurs x (Union a b) = occurs x a || occurs x b +occurs _ (Unitty) = False +occurs _ (Bottom) = False -- | Unifies two types with their most general unifier. Returns the substitution -- that transforms any of the types into the unifier. @@ -64,6 +83,17 @@ p <- unify b d q <- unify (p a) (p c) return (q . p) +unify (Times a b) (Times c d) = do + p <- unify b d + q <- unify (p a) (p c) + return (q . p) +unify (Union a b) (Union c d) = do + p <- unify b d + q <- unify (p a) (p c) + return (q . p) +unify Unitty Unitty = Just id +unify Bottom Bottom = Just id +unify _ _ = Nothing -- | Apply a substitution to all the types on a type context. applyctx :: Substitution -> Context -> Context @@ -87,7 +117,7 @@ -> Type -- ^ Constraint -> Maybe Substitution -typeinfer [] _ _ _ = Nothing +typeinfer [] _ _ _ = Nothing typeinfer [_] _ _ _ = Nothing typeinfer _ ctx (Var n) b @@ -105,16 +135,72 @@ odds [_] = [] odds (_:e:xs) = e : odds xs evens [] = [] - evens [a] = [a] + evens [e] = [e] evens (e:_:xs) = e : evens xs + typeinfer (a:x:vars) ctx (Lambda p) b = do sigma <- unify b (Arrow (Tvar a) (Tvar x)) let nctx = applyctx sigma (Map.insert 1 (sigma $ Tvar a) (incrementindices ctx)) tau <- typeinfer vars nctx p (sigma $ Tvar x) return (tau . sigma) +typeinfer (x:y:vars) ctx (Pair m n) a = do + sigma <- unify a (Times (Tvar x) (Tvar y)) + tau <- typeinfer (evens vars) (applyctx sigma ctx) m (sigma (Tvar x)) + rho <- typeinfer (odds vars) (applyctx (tau . sigma) ctx) n (tau (sigma (Tvar y))) + return (rho . tau . sigma) + where + odds [] = [] + odds [_] = [] + odds (_:e:xs) = e : odds xs + evens [] = [] + evens [e] = [e] + evens (e:_:xs) = e : evens xs + +typeinfer (y:vars) ctx (Pi1 m) a = typeinfer vars ctx m (Times a (Tvar y)) +typeinfer (x:vars) ctx (Pi2 m) b = typeinfer vars ctx m (Times (Tvar x) b) + +typeinfer (x:y:vars) ctx (Inl m) a = do + sigma <- unify a (Union (Tvar x) (Tvar y)) + tau <- typeinfer vars (applyctx sigma ctx) m (sigma (Tvar x)) + return (tau . sigma) + +typeinfer (x:y:vars) ctx (Inr m) a = do + sigma <- unify a (Union (Tvar x) (Tvar y)) + tau <- typeinfer vars (applyctx sigma ctx) m (sigma (Tvar y)) + return (tau . sigma) + +typeinfer (x:y:vars) ctx (Caseof m f g) a = do + sigma <- typeinfer (third1 vars) ctx f (Arrow (Tvar x) a) + tau <- typeinfer (third2 vars) (applyctx sigma ctx) g (Arrow (sigma $ Tvar y) (sigma a)) + rho <- typeinfer (third3 vars) (applyctx (tau . sigma) ctx) m (Union (tau . sigma $ Tvar x) (tau . sigma $ Tvar y)) + return (rho . tau . sigma) + where + third1 [] = [] + third1 [_] = [] + third1 [_,_] = [] + third1 (_:_:e:xs) = e : third1 xs + third2 [] = [] + third2 [_] = [] + third2 [_,e] = [e] + third2 (_:e:_:xs) = e : third2 xs + third3 [] = [] + third3 [e] = [e] + third3 [e,_] = [e] + third3 (e:_:_:xs) = e : third3 xs + +typeinfer _ _ Unit a = unify Unitty a + +typeinfer vars ctx (Abort m) _ = typeinfer vars ctx m Bottom + +typeinfer vars ctx (Absurd m) a = do + sigma <- unify Bottom a + tau <- typeinfer vars (applyctx sigma ctx) m Bottom + return (tau . sigma) + + -- | Type inference of a lambda expression. typeinference :: Exp -> Maybe Type typeinference e = normalize <$> (typeinfer variables emptyctx e (Tvar 0) <*> pure (Tvar 0)) @@ -136,6 +222,12 @@ Nothing -> (Map.insert m n sub, succ n) normalizeTemplate sub n (Arrow a b) = let (nsub, nn) = normalizeTemplate sub n a in normalizeTemplate nsub nn b +normalizeTemplate sub n (Times a b) = + let (nsub, nn) = normalizeTemplate sub n a in normalizeTemplate nsub nn b +normalizeTemplate sub n (Union a b) = + let (nsub, nn) = normalizeTemplate sub n a in normalizeTemplate nsub nn b +normalizeTemplate sub n Unitty = (sub, n) +normalizeTemplate sub n Bottom = (sub, n) -- | Applies a set of variable substitutions to a type to normalize it. applynormalization :: Map.Map Integer Integer -> Type -> Type @@ -143,6 +235,12 @@ Just n -> (Tvar n) Nothing -> (Tvar m) applynormalization sub (Arrow a b) = Arrow (applynormalization sub a) (applynormalization sub b) +applynormalization sub (Times a b) = Times (applynormalization sub a) (applynormalization sub b) +applynormalization sub (Union a b) = Union (applynormalization sub a) (applynormalization sub b) +applynormalization _ Unitty = Unitty +applynormalization _ Bottom = Bottom + + -- | Normalizes a type, that is, substitutes the set of type variables for -- the smaller possible ones.