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.
forall x. P(x)
thenexists 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