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.
Best Answer
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: