# How to model conditionals with first-class functions?

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?

• Well usually this can be done by encoding true and false as functions: en.wikipedia.org/wiki/Lambda_calculus#Logic_and_predicates – Willem Van Onsem May 11 '18 at 7:15
• 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. – Ezku May 11 '18 at 7:20
• 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. – Jon Purdy May 12 '18 at 2:26
• 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$. – Rodolphe Lepigre May 12 '18 at 15:05

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$$

and

$${\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.