Repository files navigation

An implementation of simply typed lambda calculus in Haskell

simple is an implementation of simply typed lambda calculus presented by Benjamin C. Pierce in hisTypes and Programming Languages. I transliterated the original source code written in OCaml into Haskell except for the parser which I rewrote inParsec.

• 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) trueparameter type mismatch at (1,19)