Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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.

share|improve this question
    
What are the semantics of simply typed $\lambda$-calculus with only function types? The version of simply typed $\lambda$-calculus I'm familiar with has product types by fiat (I think), and then its semantics are given by cartesian closed categories. From the categorical semantics point of view it's unclear what one means by having only function types because without products one can't state the usual universal property of the exponential... –  Qiaochu Yuan Dec 9 '13 at 19:20
1  
You claim that sum types can be 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 you can take 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
    
@QiaochuYuan Indeed I am trying to avoid introducing the product type by fiat. Perhaps we do not need to have full categorical semantics with products, in order to be able to write down the $\lambda$-calculus typing rules and perform computations... Also there are some papers explaining that you can define exponentials without necessarily having products. –  winitzki Dec 9 '13 at 22:00
    
@PeterLeFanuLumsdaine The question is, why cannot we have a consistent implementation of the product type? I am ready to define everything monomorphically if needed. With the sum type, there is no problem as long as we specialize choice to a fixed result type. We will then have to write separate definitions of 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

2 Answers 2

up vote 4 down vote accepted

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
share|improve this answer
    
This is quite interesting, thank you! How can I see that the disjunctions are not definable through implications within the intuitionistic logic? In the classical propositional logic, they are: $A \vee B = (B\to A)\to A$. –  winitzki Dec 10 '13 at 2:59
2  
@winitzki: In all kinds of ways. For example, all $\lor$-free formulas are Harrop, hence they have the disjunction property. Thus, if a $\lor$-free formula $C$ were equivalent to $A_0\lor A_1$, it would actually imply one of the $A_i$. But then $A_{1-i}$ also implies $A_i$. This is impossible if we e.g. take $A_0$ and $A_1$ to be distinct propositional variables. –  Emil Jeřábek Dec 10 '13 at 11:59

This is not a research question, but let me answer it anyway. You are mistaken, all functions considered are typeable:

OCaml version 4.01.0

# fun a b f -> f a b ;;
- : 'a -> 'b -> ('a -> 'b -> 'c) -> 'c = <fun>
# fun p -> p (fun x y -> x) ;;
- : (('a -> 'b -> 'a) -> 'c) -> 'c = <fun>
# fun p -> p (fun x y -> y) ;;
- : (('a -> 'b -> 'b) -> 'c) -> 'c = <fun>
# fun x f g -> f x ;;
- : 'a -> ('a -> 'b) -> 'c -> 'b = <fun>
# fun y f g -> g y ;;
- : 'a -> 'b -> ('a -> 'c) -> 'c = <fun>
# fun c f g -> c f g ;;
- : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = <fun>
share|improve this answer
    
They are typeable in a polymorphic $\lambda$-calculus, as implemented in a subset of OCaml. Not in a simply typed $\lambda$-calculus! Also, even in OCaml there is a problem if you start using these OCaml functions, - you will find that you cannot use both First and Second at the same time, because a fully constructed pair (Pair a b) gets a certain monomorphic type after you use First on it, and then you can't use Second on it. –  winitzki Dec 9 '13 at 15:03
    
I am updating the question to show OCaml code with this problem. –  winitzki Dec 9 '13 at 15:18
    
Ok, now I understand what you are asking. I will post another answer. –  Andrej Bauer Dec 9 '13 at 18:17

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.