forked fromkseo/simple
- Notifications
You must be signed in to change notification settings - Fork0
An implementation of simply typed lambda calculus in Haskell
License
NotificationsYou must be signed in to change notification settings
yy-zhong/simple
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
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)