Lambda calculus playground!

Include Standard Library

Output type

Powered by Sheepda
Read the documentation

Standard library

# Some combinators for recursion.
U = λf.(f f)
Y = λf.(λx.(x x) λx.(f λy.((x x) y)))
void = λx.(U U)

# we need numbers, so define some numbers
0 = λf.λx.x
succ = λn.λf.λx.(f (n f x))
+ = λm.λn.(m succ n)
* = λm.λn.(n (+ m) 0)
1 = (succ 0)  2 = (succ 1)  3 = (succ 2)  4 = (succ 3)  5 = (succ 4)
6 = (succ 5)  7 = (succ 6)  8 = (succ 7)  9 = (succ 8) 10 = (succ 9)
num = λa.λb.λc. (+ (+ (* (* 10 10) a) (* 10 b)) c)

# logic
true = λt.λf.t
false = λt.λf.f
if = λp.λa.λb.((p a b) p)
not = λp.λt.λf.(p f t)
and = λa.λb.(a b false)
or = λa.λb.(a true b)

# pairs
make-pair = λx.λy.λt.(t x y)
pair-first = λp.(p true)
pair-second = λp.(p false)

# more number stuff now that we have pairs
zero? = λn.(n λ_.false true)
pred = λn.
  (pair-second
    (n
     λpair.(make-pair (succ (pair-first pair)) (pair-first pair))
     (make-pair 0 0)))

- = λm.λn.(n pred m)
ge? = λm.λn.(zero? (- n m))
le? = λm.λn.(zero? (- m n))
eq? = λm.λn.(and (ge? m n) (le? m n))
/ = (Y λ/.λm.λn.
  (if (eq? m n)
      λ_. 1
      λ_. (if (le? m n)
              λ_. 0
              λ_. (+ 1 (/ (- m n) n)))))
% = λm.λn. (- m (* (/ m n) n))

# lists
nil = (make-pair false void)
nil? = λl.(not (pair-first l))
cons = λe.λl.(make-pair true (make-pair e l))
car = λl.(pair-first (pair-second l))
cdr = λl.(pair-second (pair-second l))
head = car
tail = cdr

# sequences of steps
do2 = λ_.λx.x
do3 = λ_.do2
do4 = λ_.do3
for = λn.λf.(
  (Y λrecurse.λi.
    (if (eq? i n)
        λ_. void
        λ_. (do2 (f i)
                 (recurse (succ i)))))
  0)
let = λx.λf.(f x)

# output
print-byte = PRINT_BYTE
print-list = (Y λrecurse.λl.
    (if (nil? l)
        λ_. void
        λ_. (do2 (print-byte (car l))
                 (recurse (cdr l)))))
print-newline = λ_. (print-byte (num 0 1 0))

# input
read-input = READ_BYTE
input-eof? = λp.(not (pair-first p))
input-byte = λp.(pair-second p)
read-list = (Y λrecurse.λ_.
    (let (read-input void) λb.
        (if (input-eof? b)
            λ_. nil
            λ_. (cons (input-byte b) (recurse void)))))

# itoa
zero-byte = (num 0 4 8)
itoa = λn.(
  (Y λrecurse.λn.λresult.
    (if (zero? n)
        λ_. (if (nil? result)
               λ_. (cons zero-byte nil)
               λ_. result)
        λ_. (recurse (/ n 10) (cons (+ zero-byte (% n 10)) result))))
  n nil)
print-num = λn.(print-list (itoa n))

# string stuff
string-whitespace? = λn.
    (or (or (eq? n (num 0 0 9)) (eq? n (num 0 1 0)))
        (or (eq? n (num 0 1 3)) (eq? n (num 0 3 2))))
string-lstrip = (Y λrecurse.λl.
    (if (nil? l)
        λ_. l
        λ_. (if (string-whitespace? (car l))
                λ_. (recurse (cdr l))
                λ_. l)))