An adventure in Haskell: A simple lambda interpreter

Posted on 2018 03 27 by phimuemue

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.

Goals for the project

The goals for this small tool are relatively simply to describe:

Here's a screenshot of an early version:

Screenshot of the program, during the computation of 2^2

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:

Code

The full code is hosted over there at github.