Lambda Calculus: an Elm CLI

Introduction

A Lambda Calculator

$ lambda
Welcome! type :help for help
> (\x.x) (\y.y)
λy.y
> :let id = \x.x
added id as λx.x
> id id
λx.x
# Standard Libary# Booleans
true \x.\y.x
false \x.\y.y
and \p.\q.p q p
or \p.\q.p p q
not \p.p (false) true

# Church numerals
zero \s.\z.z
one \s.\z.s z
two \s.\z.s s z
three \s.\z.s s s z
isZero \n.n (\x.zero) true
succ \n.\f.\x.f(n f x)
> and true true
λx.λy.x
> and true false
λx.λy.y
> and false false
λx.λy.y

Implementing the Calculator in Elm

type Expr
= Var String
| Lambda String Expr
| Apply Expr Expr
> :parse x
Ok (Var "x")
> :parse \x.x
Ok (Lambda "x" (Var "x"))
> :parse (\x.x) \y.y
Ok (Apply (Lambda "x" (Var "x")) (Lambda "y" (Var "y")))
(\p.\q.p q p) (\x.\y.x) (\x.\y.y)

References

Addenda

Output options

> and true false
false

> :pretty
> and true false
λx.λy.y

> :raw
> and true false
\x.\y.y

> :named
> and true false
false

:beta command

> :beta (succ zero) one
true
> :beta (\x.x) (\a.a)
true
> Omega
TOO MANY SUBSTITUTIONS (size2 > 100000). Term may be divergent
> :beta Omega Omega
LHS may be divergent

--

--

jxxcarlson on elm slack, http://jxxcarlson.github.io

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store