16
$\begingroup$

$\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.

$\endgroup$
4
  • $\begingroup$ 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... $\endgroup$ Dec 9, 2013 at 19:20
  • 2
    $\begingroup$ 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. $\endgroup$ Dec 9, 2013 at 19:27
  • $\begingroup$ @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. $\endgroup$
    – winitzki
    Dec 9, 2013 at 22:00
  • $\begingroup$ @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. $\endgroup$
    – winitzki
    Dec 9, 2013 at 22:09

2 Answers 2

9
$\begingroup$

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
$\endgroup$
2
  • $\begingroup$ 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$. $\endgroup$
    – winitzki
    Dec 10, 2013 at 2:59
  • 2
    $\begingroup$ @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. $\endgroup$ Dec 10, 2013 at 11:59
1
$\begingroup$

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

$\endgroup$
4
  • $\begingroup$ I don't understand (i) of the lemma. Is there a word missing? (Common typo.) $\endgroup$ Nov 10, 2023 at 5:31
  • $\begingroup$ "Either one of the types (is of the form...),... or the type of one of the free variables ... is of the form..." (minor edit for clarity). $\endgroup$
    – GNiklasch
    Nov 10, 2023 at 11:08
  • 1
    $\begingroup$ Edited for clarity. $\endgroup$ Nov 10, 2023 at 12:52
  • 1
    $\begingroup$ MathJax notes: using - instead of $\bullet$ tells MathJax that you want a list, and so allows it to format correctly; and you can use \label+\tag, and then \eqref, to get clickable references. I have edited accordingly. $\endgroup$
    – LSpice
    Nov 10, 2023 at 14:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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