Mathematics and Computation

A blog about mathematics for computers

How to simulate booleans in simply typed lambda calculus?

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:

  1. 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.
  2. 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.)
  3. 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.

Comments

jeremy

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

t ::= O | t -> t | t * t

Now we can define

   Boolean = Base -> Base -> Base
   true  = \(k1 :: Base) -> \(k2 :: Base) -> k1
   false = \(k1 :: Base) -> \(k2 :: Base) -> k2

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

   [[O]] = \(c::Boolean) -> c
   [[t1 -> t2]] = \(c :: Boolean) -> \(k1 :: t1) -> \(k2 :: t2) -> 
                  \(x::t1) -> [[t2]] c (k1 x) (k2 x)
   [[t1 * t2]] = \(c :: Boolean) -> \(k1 :: t1*t2) -> \(k2 :: t1*t2) ->
                  ([[t1]] c (fst k1) (fst k2), [[t2]] c (snd k1) (snd k2))

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:

{-# LANGUAGE EmptyDataDecls,PatternSignatures,GADTs,KindSignatures,ScopedTypeVariables #-}

data Base

data Type :: * -> * where
     Base  :: Type Base
     (:->) :: Type a -> Type b -> Type (a -> b)
     (:*)  :: Type a -> Type b -> Type (a, b)

type Boolean = Base -> Base -> Base

true :: Boolean
true = \(k1 :: Base) -> \(k2 :: Base) -> k1

false :: Boolean
false = \(k1 :: Base) -> \(k2 :: Base) -> k2

cond :: Type t -> Boolean -> t -> t -> t
cond Base = \(c::Boolean) -> c
cond ((t1 :: Type t1) :-> (t2 :: Type t2)) =
    \(c::Boolean) -> 
    \(k1 :: t1 -> t2) ->
    \(k2 :: t1 -> t2) -> 
    \(x :: t1) ->
        cond t2 c (k1 x) (k2 x) 
cond ((t1 :: Type t1) :* (t2 :: Type t2)) = 
    \(c::Boolean) ->
    \(k1 :: (t1, t2)) ->
    \(k2 :: (t1, t2)) ->
        (cond t1 c (fst k1) (fst k2), 
         cond t2 c (snd k1) (snd k2))
jeremy

Apologies for the poor formatting! Here's a version of "cond" without type annotations which I hope will come out better:<blockquote><pre> cond :: Type t -> Boolean -> t -> t -> t cond Base = \c -> c cond (t1 :-> t2) = \c k1 k2 x -> cond t2 c (k1 x) (k2 x) cond (t1 :* t2) = \c k1 k2 -> (cond t1 c (fst k1) (fst k2), cond t2 c (snd k1) (snd k2)) </pre></blockquote>

Andrej Bauer

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.

Andrej Bauer

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

sam

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.

Andrej Bauer

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).

sam

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.

Sridhar Ramesh

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.

How to comment on this blog: At present comments are disabled because the relevant script died. If you comment on this post on Mastodon and mention andrejbauer@mathstodon.xyz, I will gladly respond. You are also welcome to contact me directly.