# Power of existential types

It is well known that simply typed lambda calculus becomes much more expressive if you allow universal types, as in Girards system F. Thus, for example, you can encode the booleans as forall a. a -> a -> a and the integers as forall a. a -> (a-> a) -> a and furthermore, you can encode all logical operators and primitive recursive functions as well.

What happens if you use the dual concept, that of existential types? Can you encode any of the above structures? (It doesnt seem so) Can you encode any other interesting structure?

• Have you considered types of the form $(\forall x.a) \rightarrow b$? Jan 8 at 18:50
• It is well known that existential types help one encode the concept of encapsulation, e.g. $\exists X. (X \rightarrow 1)\times(\mathrm{Int}\rightarrow X)$ could encode an Int container with an "increment" operation. See e.g. dl.acm.org/doi/10.1145/44501.45065
– cody
Jan 8 at 19:56
• See the paper "Recursive types for free" for encoding of greatest fixpoints using $\exists$. homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/… Apr 1 at 13:40
• @MartinBerger I'm having trouble working with types of the form $(\forall x. a)\to b$. Not sure how to use parametricity arguments in that case. I just posted a question where I get stuck with that sort of type expression. Maybe you could help? cstheory.stackexchange.com/questions/54124 Apr 1 at 15:37

Universal types can be used to encode the least fixed point, while dually, existential types can be used to encode the greatest fixed point. For example, consider $$F(X) = 1 + A \times X$$, then the least fixed point of $$F$$ is the type of lists (of $$A$$). It is encoded by $$\forall X. (F(X) \to X) \to X$$. Expanding this you get \begin{aligned} \forall X. (F(X) \to X) \to X &= \forall X. ((1 + A \times X) \to X) \to X \\ &= \forall X. (X \times (A \to X \to X)) \to X \\ &= \forall X. X \to (A \to X \to X) \to X \\ \end{aligned} The dual notion here is potentially infinite lists, encoded by $$\exists X. X \times (X \to F(X))$$. Similarly if $$F(X) = 1 + X \times X$$ you get potentially infinite binary trees, etc.
Another interesting interaction is the relation between $$\forall$$ and $$\exists$$. We have $$(\exists X. F(X)) \to Y$$ is isomorphic to $$\forall X. F(X) \to Y$$, and with parametricity there are more interesting isomorphisms.
• The duality between $\forall$ and $\exists$ becomes even more clear when you generalise from functions to message passing. Then it becomes a clear input/output duality, see Genericity and the $\pi$-calculus with many message-passing parametricity properties. (Sorry for self-cite!) See also lots of subsequent work on polarised linear logic and session types. Jan 9 at 10:57