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?

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.

StackExchange Computer Science Q#91759, answer score: 6