diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -4,7 +4,7 @@
-**Mikrokosmos** is an untyped lambda calculus interpreter, borrowing its name from the series of
+**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.
diff --git a/mikrokosmos.cabal b/mikrokosmos.cabal
--- a/mikrokosmos.cabal
+++ b/mikrokosmos.cabal
@@ -1,5 +1,5 @@
name: mikrokosmos
-version: 0.3.0
+version: 0.4.0
synopsis: Lambda calculus interpreter
description: A didactic untyped lambda calculus interpreter.
homepage: https://github.com/M42/mikrokosmos
@@ -44,6 +44,7 @@
Interpreter
Environment
Ski
+ Types
default-language: Haskell2010
ghc-options: -Wall
diff --git a/source/Environment.hs b/source/Environment.hs
--- a/source/Environment.hs
+++ b/source/Environment.hs
@@ -17,6 +17,7 @@
, getVerbose
, getColor
, getSki
+ , getTypes
, getExpressionName
-- * Modifying the environment
@@ -24,6 +25,7 @@
, changeColor
, changeVerbose
, changeSkioutput
+ , changeTypes
-- * Filenames and Modulenames
, Filename
@@ -49,6 +51,7 @@
, verbose :: Bool
, color :: Bool
, skioutput :: Bool
+ , types :: Bool
}
-- | Default environment for the interpreter.
@@ -59,9 +62,18 @@
, verbose = False
, color = True
, skioutput = False
+ , types = False
}
+-- | Get current settings
+getColor, getVerbose, getSki, getTypes :: Environment -> Bool
+getColor = color
+getVerbose = verbose
+getSki = skioutput
+getTypes = types
+
+
-- | Adds a name binding to the environment
addBind :: Environment -> String -> Exp -> Environment
addBind env s e =
@@ -70,18 +82,6 @@
then env
else env {context = MultiBimap.insert e s (context env)}
--- | Gets the color configuration
-getColor :: Environment -> Bool
-getColor = color
-
--- | Gets the verbose configuration
-getVerbose :: Environment -> Bool
-getVerbose = verbose
-
--- | Gets the verbose configuration
-getSki :: Environment -> Bool
-getSki = skioutput
-
-- | Sets the verbose configuration on/off.
changeVerbose :: Environment -> Bool -> Environment
changeVerbose options setting = options {verbose = setting}
@@ -93,6 +93,11 @@
-- | Sets the ski output configuration on/off
changeSkioutput :: Environment -> Bool -> Environment
changeSkioutput options setting = options {skioutput = setting}
+
+-- | Sets the types output configuration on/off
+changeTypes :: Environment -> Bool -> Environment
+changeTypes options setting = options {types = setting}
+
-- | Given an expression, returns its name if it is bounded to any.
getExpressionName :: Environment -> Exp -> Maybe String
diff --git a/source/Format.hs b/source/Format.hs
--- a/source/Format.hs
+++ b/source/Format.hs
@@ -18,6 +18,7 @@
, formatName
, formatSubs1
, formatSubs2
+ , formatType
, decolor
, end
@@ -50,6 +51,9 @@
subst2Color :: Color
subst2Color = Cyan
+-- | Types are marked with this color
+typeColor :: Color
+typeColor = Yellow
-- Format sequences
-- | Sequence of characters that signals the format of a formula to the terminal.
@@ -81,6 +85,11 @@
formatSubs2 :: String
formatSubs2 = setSGRCode [SetConsoleIntensity FaintIntensity, SetColor Foreground Dull subst2Color]
+-- | Sequence of characters that signals the format of a type to the terminal.
+formatType :: String
+formatType = setSGRCode [SetConsoleIntensity NormalIntensity, SetColor Foreground Dull typeColor]
+
+
-- | Sequence of characters that cleans all the format.
end :: String
end = setSGRCode []
@@ -101,6 +110,7 @@
, formatFormula
, formatIntro
, formatName
+ , formatType
, formatPrompt
, formatLoading
, end
@@ -118,11 +128,14 @@
helpText = unlines [
formatFormula ++
"Commands available from the prompt:",
- "\t\t evaluates the expression",
- "\t:quit \t quits the interpreter",
- "\t:load \t loads the given .mkr library or script",
- "\t:verbose \t sets verbose mode on/off",
- "\t:help \t shows this help"
+ "\t\t\t evaluates the expression",
+ "\t:quit \t\t quits the interpreter",
+ "\t:load \t\t loads the given .mkr library or script",
+ "\t:verbose \t sets verbose mode on/off",
+ "\t:color \t sets color mode on/off",
+ "\t:ski \t\t sets ski mode on/off",
+ "\t:types \t untyped/simply typed lambda calculus",
+ "\t:help \t\t shows this help"
++ end
]
@@ -139,4 +152,4 @@
-- | Version
version :: String
-version = "0.3.0"
+version = "0.4.0"
diff --git a/source/Interpreter.hs b/source/Interpreter.hs
--- a/source/Interpreter.hs
+++ b/source/Interpreter.hs
@@ -27,6 +27,7 @@
import NamedLambda
import Lambda
import Ski
+import Types
-- | Interpreter action. It can be a language action (binding and evaluation)
@@ -35,10 +36,12 @@
| EmptyLine -- ^ Empty line, it will be ignored
| Error -- ^ Error on the interpreter
| Quit -- ^ Close the interpreter
+ | Restart -- ^ Restarts the environment
| Load String -- ^ Load the given file
| SetVerbose Bool -- ^ Changes verbosity
| SetColor Bool -- ^ Changes colors
| SetSki Bool -- ^ Changes ski output
+ | SetTypes Bool -- ^ Changes type configuration
| Help -- ^ Shows help
-- | Language action. The language has a number of possible valid statements;
@@ -59,9 +62,13 @@
act (EvalBind (s,le)) =
do modify (\env -> addBind env s (simplifyAll $ toBruijn (context env) le))
return [""]
-act (Execute le) =
- do env <- get
- return [unlines $
+act (Execute le) = do
+ env <- get
+ let typed = getTypes env
+ let illtyped = typed && typeinference (toBruijn (context env) le) == Nothing
+
+ return $ if illtyped then [formatType ++ "Error: not typeable expression" ++ end ++ "\n"] else
+ [ unlines $
[ show le ] ++
[ unlines $ map showReduction $ simplifySteps $ toBruijn (context env) le ] ++
[ showCompleteExp env $ simplifyAll $ toBruijn (context env) le ]
@@ -82,10 +89,17 @@
skiname = if getSki environment
then formatSubs2 ++ " ⇒ " ++ (show $ skiabs $ nameExp expr) ++ end
else ""
+ inferredtype = typeinference expr
+ typename = if getTypes environment
+ then formatType ++ " :: " ++ (case inferredtype of
+ Just s -> show s
+ Nothing -> "Type error!") ++ end
+ else ""
+ expName = case getExpressionName environment expr of
+ Nothing -> ""
+ Just exname -> formatName ++ " ⇒ " ++ exname ++ end
in
- case getExpressionName environment expr of
- Nothing -> lambdaname ++ skiname
- Just expName -> lambdaname ++ skiname ++ formatName ++ " ⇒ " ++ expName ++ end
+ lambdaname ++ skiname ++ expName ++ typename ++ end
@@ -98,10 +112,12 @@
interpreteractionParser = choice
[ try interpretParser
, try quitParser
+ , try restartParser
, try loadParser
, try verboseParser
, try colorParser
, try skiOutputParser
+ , try typesParser
, try helpParser
]
@@ -138,40 +154,30 @@
quitParser :: Parser InterpreterAction
quitParser = string ":quit" >> return Quit
+-- | Parses a "restart" command.
+restartParser :: Parser InterpreterAction
+restartParser = string ":restart" >> return Restart
+
-- | Parses a "help" command.
helpParser :: Parser InterpreterAction
helpParser = string ":help" >> return Help
--- | Parses a change in verbosity.
-verboseParser :: Parser InterpreterAction
-verboseParser = choice
- [ try verboseonParser
- , try verboseoffParser
- ]
- where
- verboseonParser = string ":verbose on" >> return (SetVerbose True)
- verboseoffParser = string ":verbose off" >> return (SetVerbose False)
-
--- | Parses a change in color.
-colorParser :: Parser InterpreterAction
-colorParser = choice
- [ try coloronParser
- , try coloroffParser
- ]
- where
- coloronParser = string ":color on" >> return (SetColor True)
- coloroffParser = string ":color off" >> return (SetColor False)
-
--- | Parses a change in ski output.
-skiOutputParser :: Parser InterpreterAction
-skiOutputParser = choice
- [ try skionParser
- , try skioffParser
+-- | Parses a change in a setting
+settingParser :: (Bool -> InterpreterAction) -> String -> Parser InterpreterAction
+settingParser setSetting settingname = choice
+ [ try settingonParser
+ , try settingoffParser
]
where
- skionParser = string ":ski on" >> return (SetSki True)
- skioffParser = string ":ski off" >> return (SetSki False)
+ settingonParser = string (settingname ++ " on") >> return (setSetting True)
+ settingoffParser = string (settingname ++ " off") >> return (setSetting False)
+-- | Multiple setting parsers
+verboseParser, colorParser, skiOutputParser, typesParser :: Parser InterpreterAction
+verboseParser = settingParser SetVerbose ":verbose"
+colorParser = settingParser SetColor ":color"
+skiOutputParser = settingParser SetSki ":ski"
+typesParser = settingParser SetTypes ":types"
-- | Parses a "load-file" command.
diff --git a/source/Main.hs b/source/Main.hs
--- a/source/Main.hs
+++ b/source/Main.hs
@@ -85,6 +85,9 @@
-- Exists the interpreter
Quit -> return ()
+ -- Restarts the interpreter context
+ Restart -> interpreterLoop defaultEnv
+
-- Unknown command
Error -> do
outputStr (if getColor environment then formatFormula else "")
@@ -116,7 +119,14 @@
end
interpreterLoop (changeSkioutput environment setting)
-
+ -- Sets the types option
+ SetTypes setting -> do
+ outputStrLn $
+ (if getColor environment then formatFormula else "") ++
+ "types: " ++ if setting then "on" else "off" ++
+ end
+ interpreterLoop (changeTypes environment setting)
+
-- Prints the help
Help -> outputStr helpText >> interpreterLoop environment
diff --git a/source/Types.hs b/source/Types.hs
new file mode 100644
--- /dev/null
+++ b/source/Types.hs
@@ -0,0 +1,150 @@
+module Types
+ ( Type (Tvar, Arrow)
+ , typeinfer
+ , typeinference
+ , normalize
+ )
+where
+
+import Control.Monad
+import Lambda
+
+import qualified Data.Map as Map
+
+-- | A type context is a map from deBruijn indices to types. Given
+-- any lambda variable as a deBruijn index, it returns its type.
+type Context = Map.Map Integer Type
+
+-- | A type variable is an integer.
+type Variable = Integer
+
+-- | A type substitution is a function that can be applied to any type
+-- to get a new one.
+type Substitution = Type -> Type
+
+-- | 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
+ 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
+
+
+-- | Creates the substitution given by the change of a variable for
+-- the given type.
+subs :: Variable -> Type -> Substitution
+subs x typ (Tvar y)
+ | x == y = typ
+ | otherwise = Tvar y
+subs x typ (Arrow a b) = Arrow (subs x typ a) (subs x typ b)
+
+-- | 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
+
+-- | Unifies two types with their most general unifier. Returns the substitution
+-- that transforms any of the types into the unifier.
+unify :: Type -> Type -> Maybe Substitution
+unify (Tvar x) (Tvar y)
+ | x == y = Just id
+ | otherwise = Just (subs x (Tvar y))
+unify (Tvar x) b
+ | occurs x b = Nothing
+ | otherwise = Just (subs x b)
+unify a (Tvar y)
+ | occurs y a = Nothing
+ | otherwise = Just (subs y a)
+unify (Arrow a b) (Arrow c d) = do
+ p <- unify b d
+ q <- unify (p a) (p c)
+ return (q . p)
+
+-- | Apply a substitution to all the types on a type context.
+applyctx :: Substitution -> Context -> Context
+applyctx = Map.map
+
+-- | The empty context.
+emptyctx :: Context
+emptyctx = Map.empty
+
+-- | Increments all the indices of a given context. It is useful for
+-- adapting the context to a new scope.
+incrementindices :: Context -> Context
+incrementindices = Map.mapKeys succ
+
+-- | Type inference algorithm. Infers a type from a given context and expression
+-- with a set of constraints represented by a unifier type. The result type must
+-- be unifiable with this given type.
+typeinfer :: [Variable] -- ^ List of fresh variables
+ -> Context -- ^ Type context
+ -> Exp -- ^ Lambda expression whose type has to be inferred
+ -> Type -- ^ Constraint
+ -> Maybe Substitution
+
+typeinfer [] _ _ _ = Nothing
+typeinfer [_] _ _ _ = Nothing
+
+typeinfer _ ctx (Var n) b
+ | Map.member n ctx = do
+ var <- Map.lookup n ctx
+ unify var b
+ | otherwise = Nothing
+
+typeinfer (x:vars) ctx (App p q) b = do
+ sigma <- typeinfer (evens vars) ctx p (Arrow (Tvar x) b)
+ tau <- typeinfer (odds vars) (applyctx sigma ctx) q (sigma (Tvar x))
+ return (tau . sigma)
+ where
+ odds [] = []
+ odds [_] = []
+ odds (_:e:xs) = e : odds xs
+ evens [] = []
+ evens [a] = [a]
+ 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)
+
+
+-- | Type inference of a lambda expression.
+typeinference :: Exp -> Maybe Type
+typeinference e = normalize <$> (typeinfer variables emptyctx e (Tvar 0) <*> pure (Tvar 0))
+
+-- | List of possible variable names.
+typevariableNames :: [String]
+typevariableNames = concatMap (`replicateM` ['A'..'Z']) [1..]
+
+-- | Infinite list of variables.
+variables :: [Variable]
+variables = [1..]
+
+
+-- | Substitutes a set of type variables on a type template for the smaller
+-- possible ones.
+normalizeTemplate :: Map.Map Integer Integer -> Integer -> Type -> (Map.Map Integer Integer, Integer)
+normalizeTemplate sub n (Tvar m) = case Map.lookup m sub of
+ Just _ -> (sub, n)
+ 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
+
+-- | Applies a set of variable substitutions to a type to normalize it.
+applynormalization :: Map.Map Integer Integer -> Type -> Type
+applynormalization sub (Tvar m) = case Map.lookup m sub of
+ Just n -> (Tvar n)
+ Nothing -> (Tvar m)
+applynormalization sub (Arrow a b) = Arrow (applynormalization sub a) (applynormalization sub b)
+
+-- | Normalizes a type, that is, substitutes the set of type variables for
+-- the smaller possible ones.
+normalize :: Type -> Type
+normalize t = applynormalization (fst $ normalizeTemplate Map.empty 0 t) t