Why is there no product type in simply typed lambda-calculus?

Question

$\DeclareMathOperator\Pair{Pair}\DeclareMathOperator\First{First}\DeclareMathOperator\Second{Second}\DeclareMathOperator\Left{Left}\DeclareMathOperator\Right{Right}\DeclareMathOperator\Choice{Choice}$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 = \mathop{\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 $(\mathop{\mathop{\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.

Answer 1

You have not really encoded the sum type $\alpha \sqcup \beta$, but made a "virtual embedding" of the sum type into $(\rho^{\rho^\beta})^{\rho^\alpha}$. You could not encode sum types in such a calculus, simply because sum types are not expressible in it (you may know this result in a different form --- disjunctions are not definable in an implicational fragment of intuitionistic propositional logic). To see how your embedding works, let me assume for a moment that our calculus has both sum and product types. Then: $$(\rho^{\rho^\beta})^{\rho^\alpha} \approx \rho^{\rho^\alpha \times \rho^\beta} \approx \rho^{\rho^{\alpha \sqcup \beta}}$$ Therefore, your embedding may be thought of as canonical morphism: $$\alpha \sqcup \beta \rightarrow \rho^{\rho^{\alpha \sqcup \beta}}$$ Actually, $\rho^{\rho^{(-)}}$ is a continuation monad, and the embedding $\tau \overset{\mathit{ret}}\rightarrow \rho^{\rho^{\tau}}$ lifts types to the continuation semantics, where as you have figured out, coproducts "virtually exist". By the way, I have said "embedding", but $\mathit{ret}$ generally is not an embedding --- it is a monomorphism if and only if $\rho$ is an internal cogenerator --- which means that the internal contravariant hom-functor $\rho^{(-)}$ is faithfull (see also this answer).

As pointed out by Peter in the comments, you may similarly "embed" product types: $$\alpha \times \beta \rightarrow \rho^{\rho^{\alpha \times \beta}} \approx \rho^{(\rho^{\beta})^\alpha}$$ Then instead of working with $\alpha \times \beta$, work with continuation type $\rho^{(\rho^{\beta})^\alpha}$. For example you may define the first projection $\rho^{(\rho^{\beta})^\alpha} \rightarrow \rho^{\rho^\alpha}$ as: $$\lambda p \colon \rho^{(\rho^{\beta})^\alpha} . \lambda f \colon \rho^\alpha . p (\lambda a \colon \alpha . \lambda b \colon \beta . f a \colon \rho)$$ and in the same manner the second projection $\rho^{(\rho^{\beta})^\alpha} \rightarrow \rho^{\rho^\beta}$ as: $$\lambda p \colon \rho^{(\rho^{\beta})^\alpha} . \lambda g \colon \rho^\beta . p (\lambda a \colon \alpha . \lambda b \colon \beta . g b \colon \rho)$$

However, it is worth saying that to emulate product types you do not need the above construction --- functions from a product type $\alpha \times \beta \rightarrow \tau$ are tantamount to functions $\alpha \rightarrow \tau^\beta$, and function to a product type $\tau \rightarrow \alpha \times \beta$ are tantamount to pairs of functions $\tau \rightarrow \alpha$ and $\tau \rightarrow \beta$, therefore in both cases are (in some sense) "redundant".

---

To not be worse, here is my GHC session:

pair :: Integer -> Bool -> (Integer -> Bool -> Bool) -> Bool
pair a b = \c -> c a b

first :: ((Integer -> Bool -> Bool) -> Bool) -> (Integer -> Bool) -> Bool
first p = \f -> p (\a b -> f a)

second :: ((Integer -> Bool -> Bool) -> Bool) -> (Bool -> Bool) -> Bool
second p = \g -> p (\a b -> g b)

*Main> let p = pair 2 True in first p ((<)1)
True
*Main> let p = pair 2 True in first p ((<)3)
False
*Main> let p = pair 2 True in second p ((||) False)
True
*Main> let p = pair 2 False in second p ((||) False)
False

Answer 2

In spite of all the interesting exchange that has gone back and forth about sum types, the original question about product types (‘how can one prove that the simply typed 𝜆-calculus does not support the product type?’) has gone unanswered. In fact, one can rigorously show the undefinability of product types in the simply typed lambda calculus. Perhaps the most obvious strategy is to use the Curry–Howard isomorphism along with the undefinablity of conjunction from implication in intuitionistic logic (a result which follows fairly straightfowardly from proof normalization). But there is also a purely type theoretic argument.

First, we note the following:

Lemma: Let $t$ be a normalized term of type $\tau_1 \rightarrow (\tau_2 \rightarrow \dotsb (\tau_n \rightarrow \phi))$. Then either one of the types $\tau_i$ is of the form $$\sigma_1 \rightarrow (\sigma_2 \rightarrow \dotsb (\sigma_n \rightarrow \phi)) \label{star}\tag{$*$}$$ or $t$ has a free variable whose type is of this form.

Proof: By induction on the construction of terms $t$ (assumed to be in normal form).

• If $t$ is a variable, the result is immediate.

• If $t$ is an application, then a simple argument shows that because it is in normal form, it must have the form $t = v(s_1)(s_2)\dotsb(s_i)$, where $v$ is a variable. The variable $v$ will have the type $\rho_1 \rightarrow (\rho_2 \rightarrow \dotsb (\rho_i \rightarrow \psi))$ where $\psi$ is the type of $t$; because the type of $t$ has the form \eqref{star}, then so does $v$, and so one of the free variables of $t$ has the form \eqref{star}.

• If $t$ is an abstraction $\lambda x^{\tau_1} (s^{\tau_2 \rightarrow \dotsb (\tau_n \rightarrow \phi)})$, apply the result to $s$ by inductive hypothesis. Then one of the following three cases holds: (i) one of $\tau_2, \dotsc, \tau_n$ has the form \eqref{star}, (ii) $x$ is a free variable of $s$ whose type $\tau_1$ has the form \eqref{star}, or (iii) some other free variable of $s$ has the form \eqref{star}. In each case the theorem holds. $\blacksquare$.

We then immediately have

Corollary: suppose there is a closed, normalized term $t$ whose type is of the form $\tau \rightarrow \phi$ where $\phi$ is an atomic type. Then $\tau$ has the form \eqref{star}.

In what follows, let $\phi_1$ and $\phi_2$ be distinct atomic types. We ask whether there are closed, typeable $\lambda$-terms $\mathtt{Pair}$, $\mathtt{First}$ and $\mathtt{Second}$ (assumed to be in normal form) such that if $x_1$ and $x_2$ are any terms of types $\phi_1$ and $\phi_2$ respectively, then

\begin{gather} \mathtt{First}(\mathtt{Pair}(x_1)(x_2)) \twoheadrightarrow_{\beta \eta} x_1 \label{star1}\tag{$*_1$} \\ \mathtt{Second}(\mathtt{Pair}(x_1)(x_2)) \twoheadrightarrow_{\beta \eta} x_2. \label{star2}\tag{$*_2$} \end{gather}

The answer is negative. To see why, looking at \eqref{star1}, we have that $\mathtt{Pair}$ must have type $\phi_1 \rightarrow (\phi_2 \rightarrow P)$ for some type $P$, and so $\mathtt{First}$ must have type $P \rightarrow \phi_1$. It follows from the Corollary that the type $P$ has the form $$\theta_1 \rightarrow (\theta_2 \rightarrow \dotsb (\theta_j \rightarrow \phi_1)). \label{star3}\tag{$*_3$}$$ But looking at \eqref{star2}, we have now that $\mathtt{Second}$ must have type $P \rightarrow \phi_2$, and so by the Corollary we have that the type $P$ has the form $$\theta'_1 \rightarrow (\theta'_2 \rightarrow \dotsb (\theta'_k \rightarrow \phi_2)). \label{star4}\tag{$*_4$}$$ But no type can have forms \eqref{star3} and \eqref{star4}.