A lambda calculus interpreter in Haskell
A few days ago, I wrote an interpreter for a small imperative language in Haskell.
Today I wrote an interpreter for one of the smallest functional languages:
the lambda calculus.
It’s small enough to show you the whole thing in one go.
module Main where data E = EApp E E | EAbs E | EVar Int -- EVar n refers to the variable bound by the nth-innermost abstraction | EInt Int -- literals deriving (Show) eval :: E -> E eval (EApp fun arg) = case eval fun of EAbs body -> eval $ sub 0 body where sub n e = case e of EApp e1 e2 -> EApp (sub n e1) (sub n e2) EAbs e' -> EAbs $ sub (n+1) e' EVar n' | n == n' -> arg -- substitute. arg has no free vars. | otherwise -> EVar n' EInt i -> EInt i other -> EApp other arg eval x = x main :: IO () main = print $ eval $ EApp (EApp (EAbs (EAbs (EVar 1))) (EInt 42)) (EInt 43)
The language itself is given by the datatype
E (for “expression”).
There are three forms of expression in the lambda calculus:
application (function calls),
In lambda calculus notation,
y are variables,
\x y. x is an abstraction (the function
fst, returning its first argument),
(\x y. x) a b is an application (calling
fst with the arguments
b, which should yield
My implementation uses “de Bruijn indexing”,
a variant of the lambda calculus which avoids explicit variable names,
instead referring identifying variables numerically.
In de Bruijn notation,
2 are variables,
\ \ 1 is an abstraction (the same function
(\ \ 1) 1 2 is an application (calling
fst with two unbound variables).
0 refers to the value bound by the innermost abstraction;
1 refers to the value bound by the second-innermost abstraction;
De Bruijn indexing simplifies implementation
by avoiding variable name clashes.
I’ve also added literal integers to the language, which are not in the pure lambda calculus. (One can encode such things using “Church encoding.”)
My Haskell function
eval is the entire interpreter.
It repeatedly evaluates function applications until no more applications can be done.
Function application is done by substitution.
The evaluation order is “lazy”:
arguments are not evaluated unless forced.
I might extend this language in future with “IO actions”, a Haskell feature, letting me write expressions which can (for example) read from standard input and write to standard output.
More by Jim
- Your syntax highlighter is wrong
- Granddad died today
- The Three Ts of Time, Thought and Typing: measuring cost on the web
- I hate telephones
- The sorry state of OpenSSL usability
- The dots do matter: how to scam a Gmail user
- My parents are Flat-Earthers
- How Hacker News stays interesting
- Project C-43: the lost origins of asymmetric crypto
- The hacker hype cycle
- The inception bar: a new phishing method
- Time is running out to catch COVID-19
- A probabilistic pub quiz for nerds
- Smear phishing: a new Android vulnerability