menu

Library of λ

Fundamental functions #

  • I = λa.a — Idiot: identity.
  • M = λa.aa — Mockingbird: omega.
  • K = λab.a — Kestrel: true, constant.
  • KI = λab.b — Kite: false, zero.
  • T = λab.ba — Thrush: not, switch.
  • W = λab.abb — Warbler: ?
  • C = λabc.acb — Cardinal: not.
  • B = λabc.a(bc) — Bluebird: compose, multiply.
  • V = λabc.cab — Vireo: pair, cons.
  • S = λabc.ac(bc) — Starling: ?

Booleans (Church-encoded) #

  • TRUE = K = λab.a — Picks the first of two inputs.
  • FALSE = KI = λab.b — Picks the second of two inputs.
  • NOT = C = λabc.acb — Swaps the second and third inputs.
  • OR = λpq.pKq — Gives the logical or of two booleans.
  • AND = λpq.pqKI — Gives the logical and of two booleans.

Natural numbers (Church-encoded) #

  • ZERO = KI — Applies a function zero times.
  • SUCC = SB = λnfx.f(nfx) — Successor: increases the value by one.
  • ONE = SUCC ZERO — Applies a function once.
  • TWO = SUCC ONE — Applies a function twice.
  • …
  • ADD = λab.a(SUCC)b — Successor of b, a times.
  • EXP = T — Swaps inputs. e.g. EXP 3 2 = 2 3 “twice thrice”.
  • MUL = B — Composes arguments in a nested fashion.

Pairs #

  • PAIR = V — Stores two values. (1, 2) represented by PAIR 1 2.
  • FST = λp.pK — Gives the first element of a pair.
  • SND = λp.pKI — Gives the second element of a pair.
  • SET_FST = λcp.V c (SND p) — Pair with value c as the first element of pair p.
  • SET_SND = λcp.V (FST p) c — Pair with value c as the second element of pair p.
  • Φ = λp.V (SND p) (SUCC (SND p)) — Increment second element, store old value as first element.

More numerals #

  • ISZERO = λn.n(K(KI))K — Is a Church numeral zero?
  • PRED = λn.FST (n Φ V((KI)(KI))) — Predecessor
  • SUB = λab.a PRED b — Subtract
  • LEQ = λab.ISZERO(SUB a b) — Less than or equal to
  • EQ = λab.AND(LEQ a b)(LEQ b a) — Equal to

Lists (cons-cell) #

  • NIL = KI — Nil, empty list [].
  • CONS = V — Cons
  • ISNIL = λl.l(K(KI))K — Is list empty?
  • HEAD = FST — Head
  • TAIL = SND — Tail
  • ELT = λnp.HEAD (n TAIL p) — Returns the nth element. Hey! That’s the site you’re on!

Lists (Church-encoded) #

  • NIL = λcn.n = KI
  • CONS = λhtcn.ch(tcn)
  • FOLD = λfzl.lfz = V — Right fold (inherent to CE lists)
  • MAP = λfl.(l (λht.CONS(fh)t) NIL)
  • FILTER = λpl. l (λht. p h (CONS h t) t) NIL
  • REVERSE = TBD
  • SUM = FOLD ADD 0
  • PRODUCT = FOLD MUL 0
  • LENGTH = FOLD (λht.SUCC t) 0

Option monad #

  • NONE = λsn.n = KI
  • SOME = λxsn.sx
  • ISSOME = λo.o(KK)KI
  • FROMMAYBE = λdo.oId

Recursion #

Y = λf.(λx.f(xx))(λx.f(xx))