20
$\begingroup$

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.

Improve this question
$\endgroup$
  • 1
    $\begingroup$ What even is the difference between universal and existential? $\endgroup$ – DeadMG Jan 2 '12 at 13:14
  • 1
    $\begingroup$ Mathematically speaking, you are right: If forall x. P(x) then exists x. P(x). Whether type systems take this into account when checking types... I have no idea. +1 for an interesting question. $\endgroup$ – delnan Jan 2 '12 at 13:27
  • 1
    $\begingroup$ @deinan: If P(x) does not hold for any x, than certainly ∀x.P(x) does not hold. What you probably meant is when there are no x, that is ∀x∈X.P(x) does not imply ∃x∈X.P(x) if X=∅. $\endgroup$ – Jan Hudec Jan 2 '12 at 14:42
  • 1
    $\begingroup$ ... And note, that if those are rewritten without set notation, they'll look different: ∀x.x∈X⇒P(x) vs. ∃x.x∈X&P(x) and that ∃x.x∈X⇒P(x) will be trivially satisfied by any x not from X. $\endgroup$ – Jan Hudec Jan 2 '12 at 14:48
  • 1
    $\begingroup$ Cool question. In Haskell it's certainly true that a value of type (forall b. Show b => b) can be passed to a function that takes a (forall b. b), but not vice-versa, implying the substitutability you'd expect from a subtyping relationship. But of course when you talk about types you should mention the type system you're looking at, particularly if you have a formal type algebra in mind for your semantics... $\endgroup$ – Owen S. Jan 8 '12 at 1:32
11
$\begingroup$

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.

Improve this answer
$\endgroup$
  • 1
    $\begingroup$ One minor, and rather late, quibble--Haskell's forall is indeed a universal quantifier in the original context of the implicit quantification it makes explicit, namely viewing polymorphic types "from the outside" for top-level definitions. On the "inside" of such a definition, when manipulating arguments, polymorphic types are effectively existential; each type variable is bound to some type, but we don't (and can't) know what that type is. To my knowledge, no Haskell implementation supports true (raw, top-level) existential types, and it's not clear to me what purpose that would even serve. $\endgroup$ – C. A. McCann Sep 4 '12 at 16:35
  • 1
    $\begingroup$ The existential types supported by GHC are types that (directly or indirectly) have universal quantifiers which, seen from "the outside", occur in contravariant position. This uses roughly the same duality as that of logical negation, so in order to have such existential types at top-level they must be doubly contravariant, using a CPS-like encoding (this is the equivalence Uday Reddy gives). Note that existential quantifiers in intuitionistic present similar inconveniences for similar reasons. $\endgroup$ – C. A. McCann Sep 4 '12 at 16:51
5
$\begingroup$

Your intuition that $\forall X.\, P(X)$ should be embeddable in $\exists X.\, P(X)$ is generally right. It only fails if the entire collection of types is empty, which is rarely the case.

However, the specific example you gave $\forall X.\, (X \times (X \to Bool))$ is not a good one. A value of this type should be able to produce an element of every type $X$ (for the first component of the pair). If you are thinking of types as sets, such a thing is not possible. So, this type is empty. It would be included in every type, in particular the existential type $\exists X.\, (X \times (X \to Bool))$, but that is not very interesting. In any case, as a theoretical exercise, here is a term that constructs such a thing:

 f (p: \forall X. (X * (X -> Bool))) = PACK X = Bool WITH p[Bool]

The article you mention for existential types is a bit theoretical. A more tutorial article is Cardelli and Wegner's paper: On understanding types, data abstraction, and polymorphism. Most advanced text books on programming languages would also have some discussion of existential types. A good book to look up would be Mitchell's Foundations of Programming Languages.

You are right that most programming languages do not have existential types explicitly. However, many do have abstract types (or by some other name such as "packages" or "modules"). So, they are able to express values of existential types, even though they don't treat such values as first-class entities.

More importantly, $\exists X.\, P(X)$ is equivalent to $\forall Y.\, (\forall X.\, P(X) \rightarrow Y) \to Y$. So, any language that treats polymorphic functions (of $\forall$ types) as first-class entities also has the ability to treat abstract types as first-class entities.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy