An adventure in Haskell: A simple lambda interpreter
I was never an expert of lambda-calculus, but I always wanted to learn (at least the basics of) it. So, I decided to write a very simplistic interpreter for the untyped lambda calculus.
- toc
Goals for the project
The goals for this small tool are relatively simply to describe:
- Simple user interface: command-line based, repl-loop-like. In particular, I wanted to help the user with manual lambda calculations. For this reason, I wanted support for some things:
- Abbreviations/macros, so that the user does not need to input too many things at once.
- Step-by-step evaluation of lambda expressions.
- Simple codebase.
- Language of choice: Haskell (using Parsec to parse user input).
Here's a screenshot of an early version:

Screenshot of the program, during the computation of \(2^2\)
As you can see, the program supports colors for specific parts of a lambda expression. A beta-reduction that's going to take place in the next step is displayed such that the function that is applied is displayed in red, while the argument is printed in blue.
Lambda expressions
A very straightforward approach to representing expressions in Haskell could look as follows:
data Expression =
Variable String
| Abstraction String Expression
| Application Expression Expression
However, I decided to equip abstractions and applications with an additional "flag" indicating whether the respective abstraction can be eta-reduced or the respective application can be beta-reduced. Variables get one additional field that contains information whether it can be expanded (i.e. if the variable name denotes a macro that stands for a - possibly more complicated - lambda expression). This results in the following declaration:
data Expression =
-- Variable may be expandable (macros)
Variable (Maybe Expression) String
-- Abstractions may be eta-convertible
| Abstraction Bool String Expression
-- Applications may be beta-convertible
| Application Bool Expression Expression
While this makes pattern matching more cumbersome in many places, it gives more freedom in other contexts: Different reduction strategies can be implemented in a more general manner and we do not have to update the color-printing routine for each reduction strategy: We simply set the corresponding flags (the ones that shall be reduced in the next step), pretty-print the expression and apply the reductions.
I also installed some smart constructors that automatically create abstractions or applications with the flag set to False
and variables without a possible expansion (i.e. Nothing
). From now on, we will also call these flags tags.
Parsing lambda expressions
I never used a Parser combinator before and was pleasantly surprised how comfortable it is to use Parsec. We can parse lambda expressions in under 40 lines of code (and I suppose this code can be improved):
variableIdentifier :: Parser String
variableIdentifier = many1 (noneOf " .\\()")
singleLambdaParser :: Parser Expression
singleLambdaParser =
(do char '\\' -- abstraction: \vars . e
spaces
vl <- (endBy1 variableIdentifier spaces)
char '.'
spaces
e <- lambdaParser
return $ foldr (\x f -> abstraction x f) e vl)
<|> (do char '(' -- parenthesized expression: (e)
e <- lambdaParser
char ')'
return e)
<|> do v <- variableIdentifier -- simple variable: v
return $ variable v
lambdaParser :: Parser Expression
lambdaParser = do l <- endBy1 singleLambdaParser spaces
return $ foldl1 (\f x -> application f x) l
parseLambda :: String -> Maybe Expression
parseLambda s = case parse lambdaParser "(unknown)" s of
Right a -> Just a
Left _ -> Nothing
Rewriting lambda expressions
Rewriting lambda expressions can be done by setting the appropriate flags in the specified fields described above. For this purpose I introduced so called "taggers" taking an expression which is untagged (i.e. no flags or possible expansions are set to non-trivial values) and possibly returning a "tagged expression".
A "tagged expression" is currently implemented as an Either Expression Expression
and we decide whether there were some newly installed tags by examining whether the tagger returned a Right
or Left
instance.
The purpose of this is that a tagger might not find any new tag to install at all, in which case it shall return the original expression wrapped in a Left
indicating that there's nothing to do.
If, on the other hand, the tagger finds something to reduce, substitute or convert, it shall wrap the resulting expression (with appropriately set tags) in a Right
indicating a "success".
To simplify wrapping and unwrapping the expressions into and from an Either
type, we have the following auxiliary functions (remember: Right
denotes "success" while Left
means "everything stays as it is" (i.e. no newly installed tags)):
type TaggedExpression = Either Expression Expression
-- unwrap expression
fromTaggedExpression :: TaggedExpression -> Expression
fromTaggedExpression (Left a) = a
fromTaggedExpression (Right a) = a
-- convert wrapped expressions to wrapped expressions
lrApplication :: Bool -> TaggedExpression -> TaggedExpression -> TaggedExpression
lrApplication b (Right f) (Right x) = Right $ Application b f x
lrApplication b (Left f) (Right x) = Right $ Application b f x
lrApplication b (Right f) (Left x) = Right $ Application b f x
lrApplication b (Left f) (Left x) = Left $ Application b f x
lrAbstraction :: Bool -> String -> TaggedExpression -> TaggedExpression
lrAbstraction b x (Right f) = Right $ Abstraction b x f
lrAbstraction b x (Left f) = Left $ Abstraction b x f
Normal-order
For now, let us simply consider how we can implement the normal order reduction. As said before, we first of all set only those tags to True
whose beta-reductions shall be done. The following code does exactly this:
normalOrderTags :: Expression -> TaggedExpression
normalOrderTags term = case term of
Application _ e@(Abstraction _ _ _) y -> Right $ Application True e y
Application _ f x -> if isRight f'
then lrApplication False f' (Left x)
else lrApplication False f' x'
where f' = normalOrderTags f
x' = normalOrderTags x
Abstraction _ x f -> lrAbstraction False x f'
where f' = normalOrderTags f
e -> Left e
The simple case distinction of normalOrderTags
works as follows: The first case describes beta-conversion while the other cases are just traversing the lambda expression and doing normalOrderTags
recursively, afterwards combining the results.
If we now want to apply all beta-reductions that we have found by using normalOrderTags
, we can use the following function:
-- applyTags takes a (possibly) tagged expression and returns an untagged one
applyTags :: Expression -> Expression
applyTags term = case term of
Variable Nothing x -> variable x
Variable (Just e) _ -> e
Application False f x -> application (applyTags f) (applyTags x)
Application True (Abstraction _ x f) y -> replaceVariable f x y
Application True f x -> error $ "Disallowed tagged application.\n" ++ (show f) ++ "\n" ++ (show x)
Abstraction False x f -> abstraction x (applyTags f)
Abstraction True _ (Application _ f _) -> applyTags f
Abstraction True _ _ -> error "Disallowed tagged abstraction."
applyTags
scans an expression and applies all tags, thereby essentially transforming ("rewriting") the lambda expression. Again, the function consists essentially of simple case distinctions, but now incorporating the value of the tag so that we can determine whether the current subterm shall be reduced or not.
Still, note that applyTags
is not bound to any specific reduction strategy - it can be used after any tagger has done work on a specific expression.
All outermost reductions
Another, more aggressive reduction strategy is to take all outermost possible reductions and perform them. The relevant code could look as follows:
allOutermostTags :: Expression -> TaggedExpression
allOutermostTags term = case term of
-- eta-reducible abstraction
Abstraction _ x e@(Application _ _ (Variable _ y)) ->
if x==y
then Right $ Abstraction True x e
else lrAbstraction False x $ allOutermostTags e
-- beta-reducible application
Application _ e@(Abstraction _ _ _) y ->
Right $ Application True e y
-- "normal stuff"
Variable _ x -> Left $ variable x
Abstraction _ x f -> lrAbstraction False x $ allOutermostTags f
Application _ f x -> lrApplication False tf tx
where tf = allOutermostTags f
tx = allOutermostTags x
Note that this does not include "nested" reductions. I.e. if we set the tag for a beta reduction, we won't set any tags for its two subexpressions.
Again, the outcome of allOutermostTags
could be fed into applyTags
to do the actual rewriting.
Interactive tagging
As I wanted the program to help with symbolic expressions, I lastly wrote an interactive tagging routine which works as follows:
confirmationMsg :: String -> [String] -> IO Char
confirmationMsg heading subs =
getSingleKeyPress $
" " ++ heading ++
concat ["\n " ++ s | s <- subs]
confirmVariableSubs :: String -> Expression -> IO TaggedExpression
confirmVariableSubs v e =
do c <- confirmationMsg ("Substitute " ++ v ++ "?") [v, show e]
case c of
'n' -> return $ Left $ variable v
_ -> return $ Right e
confirmBetaReduction :: Settings -> Expression -> Expression -> IO TaggedExpression
confirmBetaReduction settings f x =
do c <- confirmationMsg "Beta-reduce?" [show f, show x]
case c of
'n' -> do f' <- internalIteractiveTags settings f
x' <- internalIteractiveTags settings x
return $ lrApplication False f' x'
_ -> return $ Right $ betaReduce $ application f x
confirmEtaReduction :: Settings -> String -> Expression -> IO TaggedExpression
confirmEtaReduction settings x f =
do c <- confirmationMsg "Eta-convert?" [show f, x]
case c of
'n' -> do f' <- internalIteractiveTags settings f
return $ lrAbstraction False x f'
_ -> return $ Right $ etaReduce $ abstraction x f
internalIteractiveTags :: Settings -> Expression -> IO TaggedExpression
internalIteractiveTags settings expr = case expr of
Variable _ v -> case variableAbbreviationTag settings expr of
Left v' -> return $ Left v'
Right e -> confirmVariableSubs v e
Application _ f x -> if betaDirectlyReducible expr
then confirmBetaReduction settings f x
else (do f' <- internalIteractiveTags settings f
x' <- internalIteractiveTags settings x
return $ lrApplication False f' x')
Abstraction _ x f -> if etaDirectlyReducible expr
then confirmEtaReduction settings x f
else (do f' <- internalIteractiveTags settings f
return $ lrAbstraction False x f')
interactiveTags :: Settings -> Expression -> IO TaggedExpression
interactiveTags settings expr = do putStrLn $ "! " ++ (show expr)
internalIteractiveTags settings expr
Core of this method is internalInteractiveTags
which takes an additional variable settings
containing (among other things) an "environment", i.e. a mapping from macros to lambda expressions. Using this, we are able to deal with macros. Again, it consists of a simple case distinction to determine if we can apply some rewriting. If so, the algorithm asks for confirmation whether it should apply the possible conversion (via confirmVariableSubs
, confirmBetaReduction
and confirmEtaReduction
). The interactive tagger - of course - can not simply return a TaggedExpression
but must use an IO TaggedExpression
since it involves user interaction (which basically is input/output).
Aftermath
Looking back and reconsidering my original goals, I conclude the following:
- Parsing the expression was unexpectedly comfortable using parsec.
- The code base is already quite unmaintainable which I accredit to my very limited experience in Haskell.
Code
The full code is hosted over there at github.