Since languages with recursible first-class functions are Turing-complete, they should be able to express anything expressible in any other programming language. Therefore, it should be possible to model conditional expressions (i.e. if-statements) with first-class functions. Could someone illustrate how to do this?

  • $\begingroup$ Well usually this can be done by encoding true and false as functions: en.wikipedia.org/wiki/Lambda_calculus#Logic_and_predicates $\endgroup$ May 11, 2018 at 7:15
  • $\begingroup$ This is called Church Encoding: en.m.wikipedia.org/wiki/Church_encoding That’s a really good keyword to start your search, and there should be quite a few tutorials on the subject too. Personally, I found ”Programming with nothing” a good hands-on exercise. $\endgroup$
    – Ezku
    May 11, 2018 at 7:20
  • $\begingroup$ Church encoding works to construct data types in untyped lambda calculus. The related Böhm–Berarducci Encoding, introduced in Automatic synthesis of typed Λ-programs on term algebras, gives a way of translating algebraic data types systematically to typed lambda calculus (System F) that also lets you easily eliminate (pattern-match) on the values. $\endgroup$
    – Jon Purdy
    May 12, 2018 at 2:26
  • $\begingroup$ Church encoding also works perfectly in the typed setting of System F. For instance, Church booleans can be given the type $\forall X.X → X → X$, and Church naturals can be given the type $\forall X.(X → X) → X → X$. $\endgroup$ May 12, 2018 at 15:05

1 Answer 1


The usual encoding of booleans, due to Church, is

$$ {\sf true} = \lambda x. \lambda y. x \qquad {\sf false} = \lambda x. \lambda y. y $$

Roughly, "true" is the function which takes two arguments $x,y$ (first takes $x$, then also takes $y$) and returns the first one. Instead, "false" returns the second one.

If-then-else is then encoded as applying an encoded boolean to the "then" and "else" branches. In this way, the boolean chooses the right value to return.

$$ {\sf if}\ b\ {\sf then}\ t\ {\sf else}\ e = b\, t\, e $$

It is then easy to check the so-called "$\beta$" laws:

$$ {\sf if\ true\ then}\ t\ {\sf else}\ e = {\sf true}\, t\, e = (\lambda x.\lambda y.x)\, t\, e = (\lambda y.t)\, e = t $$


$$ {\sf if\ false\ then}\ t\ {\sf else}\ e = {\sf false}\, t\, e = (\lambda x.\lambda y.y)\, t\, e = (\lambda y.y)\, e = e $$

Essentially, these laws state what happens when you "construct" a boolean (using the constants $\sf true, false$), and then "destruct" it later on (using it in an $\sf if\ then\ else$).

Using functions in this way, one can write encodings for all the usual data types, like naturals, pairs, variants, lists, trees, etc.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.