packages feed

mikrokosmos 0.4.0 → 0.5.0

raw patch · 8 files changed

+310/−76 lines, 8 files

Files

README.md view
@@ -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).
mikrokosmos.cabal view
@@ -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
source/Format.hs view
@@ -152,4 +152,4 @@  -- | Version version :: String-version = "0.4.0"+version = "0.5.0"
source/Interpreter.hs view
@@ -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 ] ++
source/Lambda.hs view
@@ -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
source/NamedLambda.hs view
@@ -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.
source/Ski.hs view
@@ -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
source/Types.hs view
@@ -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.