Consider simply typed $\lambda$-calculus that has only the unit type as primitive. We would like to encode the product and the sum types. An encoding of the product type in the untyped $\lambda$-calculus is this:

Pair = $\lambda a.\lambda b.\lambda f. f\ a\ b$

First = $\lambda p. p (\lambda x. \lambda y.x)$

Second = $\lambda p. p (\lambda x. \lambda y.y)$

Then p = Pair a b is a fully constructed pair, of which we can compute (First p) to recover a and (Second p) to recover b.

However, this construction cannot be given a consistent type in simply typed $\lambda$-calculus. The immediate problem is the type of $f$ that cannot be consistently assigned, because First and Second will not, in general, have equal types if $a$ and $b$ have different types. If $a$ has type $\alpha$ and $b$ has type $\beta$ then $f$ needs to have type $\alpha\to\beta\to\alpha$ and at the same time $\alpha\to\beta\to\beta$. This forces us to have $\alpha=\beta$, or else the types are inconsistent.

Well, if this construction does not work then maybe another one will work. But it seems to me that nothing can work here. It is not possible to define some $\lambda$-terms with consistent types to implement the product type.

How can one *prove* that the simply typed $\lambda$-calculus does not support the product type? Equivalently, to show that the category of types in this calculus does not contain product objects for unequal types. Equivalently, to show some appropriate statement about propositions that will follow from the Curry-Howard isomorphism. Equivalently, to show that some formula is not deducible in the intuitionistic logic... What is the method that can derive this kind of statement rigorously? Where can I find such a proof if it is readily found?

It is interesting to note that the sum type *can* be encoded in simply typed $\lambda$-calculus without such problems.

Left = $\lambda x.\lambda f. \lambda g.f\ x$

Right = $\lambda y.\lambda f. \lambda g.g\ y$

Choice = $\lambda c.\lambda f. \lambda g.c\ f\ g$

If we assume that $x$ has type $\alpha$ and $y$ has type $\beta$, while (Choice c f g) returns a result of type $\rho$, it is straightforward to assign types consistently to Left, Right, and Choice.

Why is it that the product type is impossible (if this is true) while the sum type can be encoded?

PS

Here is an OCaml code that illustrates the problem with the product type.

```
# let pair (a:int) (b:bool) = fun f -> f a b;;
val pair : int -> bool -> (int -> bool -> ’a) -> ’a = <fun>
# let first p = p (fun (x:int)(y:bool) -> x);;
val first : ((int -> bool -> int) -> ’a) -> ’a = <fun>
# let p1 = pair 1 true;;
val p1 : (int -> bool -> ’_a) -> ’_a = <fun>
# first p1;;
- : int = 1
# let second p = p (fun (x:int)(y:bool) -> y);;
val second : ((int -> bool -> bool) -> ’a) -> ’a = <fun>
# second p1;;
Error: This expression has type (int -> bool -> int) -> int
but an expression was expected of type (int -> bool -> bool) -> ’a
# p1;;
- : (int -> bool -> int) -> int = <fun>
```

After applying `first`

to a fully constructed pair `p1`

, the type of the pair becomes monomorphic, and we cannot use `second`

on `p1`

anymore. (Here I am telling OCaml that `x`

and `y`

are monomorphic and have particular types, in order to simulate the simply typed $\lambda$-calculus in Ocaml. If OCaml had a monomorphic, i.e. simply typed, implementation of $\lambda$-calculus, we would not be able to define `pair`

, `first`

, `second`

at all.)

Here is OCaml code for implementing the sum type.

```
# let left (x:int) (f:int->bool)(g:unit->bool) = f x;;
val left : int -> (int -> bool) -> (unit -> bool) -> bool = <fun>
# let right (x:unit) (f:int->bool)(g:unit->bool) = g x;;
val right : unit -> (int -> bool) -> (unit -> bool) -> bool = <fun>
# let case (c:(int -> bool) -> (unit -> bool) -> bool) f g = c f g;;
val case :
((int -> bool) -> (unit -> bool) -> bool) ->
(int -> bool) -> (unit -> bool) -> bool = <fun>
# let la = left 1;;
val la : (int -> bool) -> (unit -> bool) -> bool = <fun>
# let rb = right ();;
val rb : (int -> bool) -> (unit -> bool) -> bool = <fun>
# case la (fun x->x=1) (fun y->false);;
- : bool = true
# case rb (fun x->x=1) (fun y->false);;
- : bool = false
```

Note that `case`

, `right`

, `left`

have been fully specified and are never polymorphic.

canbe encoded in this way, but I’m not convinced. Your sum type is essentially based on the polymorphic encoding $\alpha + \beta := \forall \rho,\, (\alpha \to \rho) \to (\beta \to \rho) \to \rho$, just as your product is based on $\alpha \times \beta := \forall \rho,\, (\alpha \to \beta \to \rho) \to \rho$. Now, it’s true as you say that youcantake a single instantiation of $\rho$ in $\alpha + \beta$ and keep`left`

,`right`

, and`choice`

all well-typed. However, with this instantiation, it’s no longer a sum type:`choice`

has been specialized too far. – Peter LeFanu Lumsdaine Dec 9 '13 at 19:27`choice`

for different types. I am going to update the post to include OCaml code for this. But nothing works at all with the product type. My two questions still stand. – winitzki Dec 9 '13 at 22:09