Introduction

Haskell implementation of the lambda calculi covered in the Types and Programming Languages book. Work in progress.

A web REPL / tutorial based on this is available here. In case you wonder, the code for this can be found in the browser branch.

As of today, 2 variants of lambda calculus are covered: the regular untyped lambda calculus, and the simply typed lambda calculus.

How to run it

The following command will fire an untyped lambda calculus REPL.

stack run untyped

The following command will fire a simply typed lambda calculus REPL.

stack run typed

Examples: untyped lambda calculus

> \x.x
\x.x
> \t.\f.t
\t.\f.t
> (\t.\f.\t) (\x.x) (\x.x x)
\x.x
> id = \x.x
()
> id \t.\f.t
\t.\f.t

Examples: simply typed lambda calculus

Note: to avoid grammar ambiguity problems, the application is done via the $ operator.

> \x : Bool.true
\x:Bool.true : Bool->Bool
> \x : Nat.succ x
\x:Nat.succ x : Nat->Nat
> (\x : Bool. if x then 0 else succ 0) $ false
succ 0 : Nat
> (\x : Bool. if x then 0 else succ 0) $ 0
ArgMisMatch {expected = Bool, got = Nat}

Options (Untyped only)

2 evaluations strategies are supported: call by value and full beta reduction. The main difference is that the latter will reduce the expressions fully, while call by value will not reduce anything inside abstractions.

Evaluation strategy

> :beta
Switching to full beta evaluation mode.
> \x.(\x.x) x
\x.x
> :cbv
Switching to call by value evaluation mode.
> \x.(\x.x) x
\x.(\x.x) x

Verbose mode

It is possible to display all the reduction steps:

> :verbose on
Enabling verbose mode.
> (\x.\y.y) (\s.\z.z) (\x.(\x.x) x)
(\x.\y.y) \s.\z.z \x.(\x.x) x
(\y.y) \x.x
\x.x
> :verbose off
Disabling verbose mode.

Status

Language features

• Untyped lambda calculus
• Simply typed lambda calculus
• Simple extensions (Let bindings, records, sum types ...)
• Subtyping
• Recursive types
• Polymorphism
• Higher-Order systems

Project features

• A CLI REPL
• A web REPL
• 2 evaluation strategies supported: Call by value and full beta reduction
• possibility to print all the reduction steps
• Variable assignment feature
• Simply typed lambda calculus

...