2
$\begingroup$

Of course, it isn't possible to construct them directly since we hasn't these type constructors, but only function constructor (arrow). But suppose there are 2 types $A$ and $B$, from which we need to create a product (or tuple) type $A*B$ and also sum type $A+B$.

Let's remember the algebra of types: functional type $A \rightarrow B$ is equivalent to exponentiation: $B^A$. Now we need to create some kind of composite type in which addition and multiplication can ultimately be replaced solely by exponents, so we encode the sum and the product.

$P^{A*B} = (P^B)^A \Leftrightarrow (A*B) \rightarrow P = A \rightarrow B \rightarrow P$ (functional constructor is right-associative)

and

$P^{P^{A+B}} = P^{P^A*P^B} = (P^{P^B})^{P^A} \Leftrightarrow ((A+B) \rightarrow P) \rightarrow P = ((A \rightarrow P)*(B \rightarrow P)) \rightarrow P = (A \rightarrow P) \rightarrow (B \rightarrow P) \rightarrow P$

In this answer, the last technique is called "virtual embedding" by continuation. At the same time, I also heard about some theorems about the non-existence of conjunction and disjunction in implicative propositional logic, but I don't understand why these "virtual" products and sums aren't counted. (According to the Curry-Howard isomorphism, everything demonstrated regarding type theory also works in implicative logic).

Where am I going wrong?

$\endgroup$
1
  • $\begingroup$ What is a virtual embedding? $\endgroup$ Commented Dec 19, 2023 at 23:26

2 Answers 2

7
$\begingroup$

A phrase like "it is not possible to encode product types in the simply-typed $\lambda$-calculus (without product types)" means: it is not true that for every type $A$ and type $B$, there exists some type $X$ such that $X$ is (isomorphic to) the product of $A$ and $B$. It does not mean that there exist no types that are isomorphic to a type involving a product (in a calculus having product types).

For instance, you are correct that, for all types $A, B, P$ in the simply-typed $\lambda$-calculus with products, we have that $P^{A \times B}$ is isomorphic to $(P^B)^A$, so that we can encode the former type with the latter type when we do not have products. But we cannot construct a type isomorphic to $A \times B$ alone.

$\endgroup$
2
$\begingroup$

You're looking for Church encodings, which are encodings of type constructions and datatypes in the polymorphic $\lambda$-calculus. That is, apart from having function types $\to$ we also need $\forall$ to quantify over all types.

For example, let us take your observation that $$((A + B) \to P) \to P) = (A \to B) \to (B \to P) \to P.$$ If we keep $P$ fixed then this is not very useful, but if we make sure that $P$ is arbitrary then it works: $$A + B = \forall P .\, (A \to B) \to (B \to P) \to P.$$ The other observation of your works also to give $$A \times B = \forall P .\, A \to B \to P.$$ And here are the natural numbers: $$\mathbb{N} = \forall P .\, (P \to P) \to (P \to P),$$ The unit type is $1 = \forall P .\, P \to P$, the empty type is $0 = \forall P.\, P$, and so on.

This is just the basic idea. The topic has been studied by many people and there are lots of things to learn here. The Wikipedia links are a decent starting point.

$\endgroup$

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.