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.
Here’s Main.hs
:
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:
abstraction (functions),
application (function calls),
and variables.
In lambda calculus notation,
x
and 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 a
and b
, which should yield a
).
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,
1
and 2
are variables,
\ \ 1
is an abstraction (the same function fst
),
and (\ \ 1) 1 2
is an application (calling fst
with two unbound variables).
The variable 0
refers to the value bound by the innermost abstraction;
the variable 1
refers to the value bound by the second-innermost abstraction;
et cetera.
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
What does the dot do in JavaScript?
foo.bar
, foo.bar()
, or foo.bar = baz
- what do they mean? A deep dive into prototypical inheritance and getters/setters. 2020-11-01
Smear phishing: a new Android vulnerability
Trick Android to display an SMS as coming from any contact. Convincing phishing vuln, but still unpatched. 2020-08-06
A probabilistic pub quiz for nerds
A “true or false” quiz where you respond with your confidence level, and the optimal strategy is to report your true belief. 2020-04-26
Time is running out to catch COVID-19
Simulation shows it’s rational to deliberately infect yourself with COVID-19 early on to get treatment, but after healthcare capacity is exceeded, it’s better to avoid infection. Includes interactive parameters and visualizations. 2020-03-14
The inception bar: a new phishing method
A new phishing technique that displays a fake URL bar in Chrome for mobile. A key innovation is the “scroll jail” that traps the user in a fake browser. 2019-04-27
The hacker hype cycle
I got started with simple web development, but because enamored with increasingly esoteric programming concepts, leading to a “trough of hipster technologies” before returning to more productive work. 2019-03-23
Project C-43: the lost origins of asymmetric crypto
Bob invents asymmetric cryptography by playing loud white noise to obscure Alice’s message, which he can cancel out but an eavesdropper cannot. This idea, published in 1944 by Walter Koenig Jr., is the forgotten origin of asymmetric crypto. 2019-02-16
How Hacker News stays interesting
Hacker News buried my post on conspiracy theories in my family due to overheated discussion, not censorship. Moderation keeps the site focused on interesting technical content. 2019-01-26
My parents are Flat-Earthers
2019-01-20
The dots do matter: how to scam a Gmail user
Gmail’s “dots don’t matter” feature lets scammers create an account on, say, Netflix, with your email address but different dots. Results in convincing phishing emails. 2018-04-07
The sorry state of OpenSSL usability
OpenSSL’s inadequate documentation, confusing key formats, and deprecated interfaces make it difficult to use, despite its importance. 2017-12-02
I hate telephones
I hate telephones. Some rational reasons: lack of authentication, no spam filtering, forced synchronous communication. But also just a visceral fear. 2017-11-08
The Three Ts of Time, Thought and Typing: measuring cost on the web
Businesses often tout “free” services, but the real costs come in terms of time, thought, and typing required from users. Reducing these “Three Ts” is key to improving sign-up flows and increasing conversions. 2017-10-26
Granddad died today
Granddad died. The unspoken practice of death-by-dehydration in the NHS. The Liverpool Care Pathway. Assisted dying in the UK. The importance of planning in end-of-life care. 2017-05-19
How do I call a program in C, setting up standard pipes?
A C function to create a new process, set up its standard input/output/error pipes, and return a struct containing the process ID and pipe file descriptors. 2017-02-17
Your syntax highlighter is wrong
2014-05-11
Tagged #programming. All content copyright James Fisher 2018. This post is not associated with my employer. Found an error? Edit this page.