An implementation of untyped lambda calculus in Haskell
untyped is an implementation of untyped lambda calculus presented by Benjamin C. Pierce in his Types and Programming Languages. I transliterated the original source code written in OCaml into Haskell except for the parser which I rewrote in Parsec.
- Variables:
x - Applications:
x x - Lambda abstractions:
\x.x
- The representation of a variable is a number - its De Brujin index
- Evaluation performs substitution
- Pretty printer removes redundant parenthesis
untypedi is a REPL where you can input a lambda calculus term.
% (\x.x) (\x.x)
\x.x
% (\x.y)
Invalid lambda caluclus: (\x.y)