An implementation of simply typed lambda calculus in Haskell
simple is an implementation of simply typed 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
- Conditional: if x then y else z
- Booleans: true, false
- The representation of a variable is a number - its De Brujin index
- Evaluation performs substitution
simplei is a REPL where you can input a lambda calculus term.
% \x:Bool.x
(\x:Bool.x)
$ (\x:Bool->Bool.x) true
parameter type mismatch at (1,19)