Are universal types a sub-type, or special case, of existential types?

I would like to know whether a universally-quantified type $T_a$: $$T_a = \forall X: \left\{ a\in X,f:X→\{T, F\} \right\}$$ is a sub-type, or special case, of an existentially-quantified type $T_e$ with the same signature: $$T_e = \exists X: \left\{ a\in X,f:X→\{T, F\} \right\}$$

I’d say “yes”: If something is true “for all X” ($\forall X$), then it must also be true “for some X” ($\exists X$). That is, a statement with ‘$\forall$’ is simply a more restricted version of the same statement with ‘$\exists$’: $$∀X, P(X) \overset?\implies ∃X, P(X).$$

Am I wrong somewhere?

Background: Why am I asking this?

I am studying existential types in order to understand why and how “Abstract [Data] Types Have Existential Type”. I cannot get a good grasp of this concept from theory alone; I need concrete examples, too.

Unfortunately, good code examples are hard to find because most programming languages have only limited support for existential types. (For instance, Haskell’s forall, or Java’s ? wildcards.) On the other hand, universally-quantified types are supported by many recent languages via “generics”.

What’s worse, generics seems to easily get mixed up with existential types, too, making it even harder to tell apart existential from universal types. I’m curious why this mix-up occurs so easily. An answer to this question might explain it: If universal types are indeed only a special case of existential types, then it’s no wonder that generic types, e.g. Java’s List<T>, can be interpreted either way.

Answer

First, from a mathematical point of view, $\forall x:T, P(x)$ does not imply $\exists x:T,P(x)$. The implication holds if and only if $T$ is not empty. However, in programming languages, it is uncommon to deal with empty types (though it happens).

Still from a mathematical point of view, even when $(\forall x:T, P(x)) ⇒ (\exists x:T, P(x))$, the two are not the same. If you give types a set semantics, then $T_a$ is a superset of $T_e$, not the same type. (Actually it’s not a superset; it’s close to isomorphic to a superset.)

Let’s get closer to programming language theory and see what these types actually mean. $T_a = ∀X.\{a: X, f: X\rightarrow\mathsf{bool}\}$ is a universal type: if you have a value $A$ of that type, you can construct $A(M)$ for any $M:X$. In particular, if you have $M_1$ and $M_2$ both of type $X$, you can construct $A(M_1)$ and $A(M_2)$. In essence (and possibly in effect, depending on the language) $T_a$ is a function from types to terms. As such, the universal type provides type parametrization: one value working for all types. Universal types are at the heart of polymorphism.

The existential type $T_e = \exists X.\{a: X, f: X\rightarrow\mathsf{bool}\}$ is quite a different beast. Given a value $B$ of type $T_e$, there is only one term $N: X$ such that $\pi_1(B) = N$, and for this term $\pi_2(B) = \{a:N, f:N\rightarrow\mathsf{bool}\}$. The existential type provides a way to hide the nature of $N$; it’s saying, “There exists a type! But I won’t tell you which!”. As such, the existential type provides type abstraction: one specific hidden value. Existential types are at the heart of module systems.

Don’t get mislead by Haskell’s forall: despite its name, it’s a form of existential quantifier.

For background, I strongly recommend Types and Programming Languages (chapters 23 and 24 discuss universal types and existential types respectively). It’s will provide useful background to understand research articles.

Attribution
Source : Link , Question Author : Community , Answer Author : Gilles ‘SO- stop being evil’

Leave a Comment