I have been writing lecture notes on computable mathematics. One of the questions that came up was whether it is possible to simulate the booleans in the simply-typed $\lambda$-calculus. This is a nice puzzle in functional programming. If you solve it, definitely let me know, although I suspect logicians did it a long time ago.

The simply-typed $\lambda$-calculus is a purely functional language in which we have a single base type, functions, and pairs. In this language every term normalizes, so we cannot write a non-terminating program, and it does not matter whether we evaluate eagerly or lazily. To make things more concrete, let me rephrase this as a fragment of Haskell (Ocaml or ML would do just as well). We may use *only the following constructs*:

- An abstract “base” type, which is traditionally denoted by
*O*(the letter). In Ocaml this would be a type whose implementation is hidden by a signature. I am not quite sure what it is in Haskell, but it could be a type parameter about which nothing is known. For practical purposes we may take*O*to be*Int*and make sure we do not use anything specific about*Int*. - Functions: we may form functions by $\lambda$-abstraction and apply them. Very importantly,
*all variables must be explicitly typed (polymorphism is forbidden).*For example, it is ok to write`\(x :: O) -> x`

but not`\x -> x`

because that would be polymorphic. (We must include the pragma`{-# LANGUAGE PatternSignatures #-}`

in Haskell code to allow explicitly typed variables.) - Pairs: we may form pairs and use the projections
`fst`

and`snd`

. This is really just a convenience, because we can always eliminate pairs by currying.

The question is this: is there a type *Boolean* (constructed from the base type *O* using function types and product types) with values

true :: Boolean false :: Boolean

and for each type `t`

a constant

cond_t :: Boolean -> t -> t -> t

such that, for all `x`

and `y`

of type `t`

:

cond_t true x y = x cond_t false x y = y

Notice that since polymorphism is forbidden, we have a family of constants `cond_t`

, one for each type `t`

, that simulate the conditional statement.

#### Booleans via polymorphism

If we allow polymorphic functions, the booleans may be defined thus:

type Boolean t = t -> t -> t true, false :: Boolean t true x y = x false x y = y cond :: Boolean t -> t -> t -> t cond b x y = b x y

Of course, since we have polymorphism a single `cond`

does the job.

I suspect the answer is negative and the booleans cannot be simulated.

I don’t know whether this is the solution you’re after, but it seems to be possible to define cond_t inductively over types. The grammar of types is

Now we can define

and cond at type t by the function [[-]] where (using a Haskelly

notation)

Now we have a single definition of Boolean and we can obtain cond_t

for any particular t. In fact, we can define cond in Haskell using GADTs:

Apologies for the poor formatting! Here’s a version of “cond” without type annotations which I hope will come out better:

Excellent, thanks. This looks good to me and provides some ideas on how to attack the more general question, whether every typed PCA has booleans. A typed PCA is like lambda-calculus except the types are not necessarily generated inductively (there may be a single type so that one particular example is the untyped lambda calculus), and application is potentially partial. Now I know that if there is a typed PCA without sums, its types must not be inductively generated.

P.S. I took the liberty of reformatting your posts so that the code is readable.

How about `lambda`-calculus with two basic types? Do we get booleans then?

We do get booleans if we have pairs:

type Boolean = (O -> O -> O, I -> I -> I)

true = (\x y -> x, \x y -> x)

false = (\x y -> y, \x y -> y)

…

though the Boolean type now also includes the nonsense terms

(\x y -> x, \x y -> y) and (\x y -> y, \x y -> x)

We can prove that it is impossible to define booleans without pairs.

Suppose we have the two base types: O and I, a type Boolean, closed terms

true and false, and for every type t a closed term cond_t such that:

true :: Boolean

false :: Boolean

cond_t :: Boolean -> t -> t -> t

cond_t true x y = x

cond_t false x y = y

Let’s consider the body, M, of cond_O.

cond_O :: Boolean -> O -> O -> O

cond_O = \b x y.M

Without loss of generality we can assume that M is in beta-normal

form. As M has base type it cannot be a lambda, so it must be of the

form:

z M1 … Mn

for some variable z and terms M1, … Mn. Now, z cannot be a free

variable as then we would have:

cond_O true x y = z M1 … Mn =/= x

So z must be b, x or y. If it were x or y then n would have to be 0 as

x and y have base type. In the former case this gives

cond_O false x y = x =/= y

and in the latter

cond_O true x y = y =/= x

Therefore it must be the case that z = b. So

cond_O b x y = b M1 … Mn : O

Hence, for some types t1, …, tn

Boolean = t1 -> … -> tn -> O

The same argument applied to cond_I means that for some types t1′,

…, tm’:

Boolean = t1′ -> … -> tm’ -> I

which gives a contradiction.

I saw how to get booleans for two basic types after I asked the question. Your proof looks good to me, thanks. So the new candidate for a lambda calculus with products and no booelans is lambda calculus with infinitely many base types, but I don’t see at the moment how to prove that it does not have booleans. Actually, I should just find a cartesian closed category in which the coproduct 1+1 does not exist, that would do it, as well.

P.S. I am not worried about the type of booleans containing garbage. Most types contain garbage anyway (such as the undefined element).

Here’s a proof sketch to show that simply-typed lambda calculus with

products and infinitely many base types does not have booleans.

The key idea is to show that if we can define booleans then the

Boolean type must contain every base type as a subformula, and

therefore must be infinite. Infinite types are not allowed, hence we

cannot define a Boolean type. (If we do allow infinite types and

infinite terms then it is easy to define a Boolean type.)

Let’s assume our base types are:

O1, O2, …

The grammar of (beta) normal forms is defined mutually recursively

with that of neutral forms:

(normal forms) M ::= \x.M | | N

(neutral forms) N ::= x | N M | fst N | snd N

Consider the form of the body of the conditional (reduced to beta

normal form) at each base type Oi:

cond_Oi b x y = Mi

cond_Oi true x y = x

cond_Oi false x y = y

As Mi has base type it must be a neutral form. We define the head

variable of a neutral form as follows:

hd (x) = x

hd (N M) = hd N

hd (fst N) = hd N

hd (snd N) = hd N

It’s not difficult to show that hd Mi = b (it can’t be free, x, or y,

so it must be b).

By induction over the structure of typing derivations we can show

that: if G |- N:A and G |- hd N:T then A is a subformula of T.

Hence, Oi is a subformula of Boolean for every i, and Boolean must

have an infinite type.

You mention looking for a cartesian closed category in which the coproduct 1 + 1 does not exist. Examples of this are easy enough; e.g., let FinSet be the CCC of sets of natural number cardinality, and consider the full subcategory containing all such sets except those of cardinality 2. This is readily observed to be a sub-CCC [by the primality of 2]; however, it cannot contain a contain a coproduct 1 + 1. For, if a set of cardinality n were this coproduct, then the number of maps from n to, say, the three element set would have to be both 3^n and 3^2, but from this it would follow that n = 2.