All you need is a lambda

Little experiments with lambda calculus. As of now there are two different implementations of lambda calculus. There is a vanilla one that is just a straight implementation of lambda calculus as descibed by Alonzo Church. On top of that there is an "Enhanced" lambda calculus that also supports let statements.

Also, there are two interpreters(a.k.a reducers): deBruijnInterpreter that uses De Bruijn Index and therefore is strict in the sense that all the referenced variables must be in scope before referencing them. The second one is dynamicInterpreter that allows to reference not yet defined variables.

For example (λfoo. (foo x) b)(λx y. y (x x)) will reduce to x (b b) if using deBruijnInterpreter, but it will reduce to b (b b) when using dynamicInterpreter.

Quickstart

Be sure to have stack installed.

$ stack build
$ stack exec lc
λ >> λx.x
λx.x
λ >> (λx.x) a
a
λ >> mytrue = \x y. x
λx.λy.x
λ >> myfalse = \x y. y
λx.λy.x
λ >> true
λx.λy.x
λ >> false
λx.λy.y
λ >> true t f
t
λ >> false t f
f
λ >> (not true) t f
f
λ >> 0
λf.λx.x
λ >> 0 f x
x
λ >> (succ 0) f x
f x

Stdlib

The repl also provides a limited form of standard library. Here are some bindings:

• id, const and s also called SKI combinators
• omega and Y combinators
• church booleans
• church integers

Feel free to grep for stdLib in app/Main.hs though 😉.