What is an existential type?

A value of an existential type like ∃x. F(x) is a pair containing some type x and a value of the type F(x). Whereas a value of a polymorphic type like ∀x. F(x) is a function that takes some type x and produces a value of type F(x). In both cases, the type closes over some type constructor F.

Note that this view mixes types and values. The existential proof is one type and one value. The universal proof is an entire family of values indexed by type (or a mapping from types to values).

So the difference between the two types you specified is as follows:

T = ∃X { X a; int f(X); } 

This means: A value of type T contains a type called X, a value a:X, and a function f:X->int. A producer of values of type T gets to choose any type for X and a consumer can't know anything about X. Except that there's one example of it called a and that this value can be turned into an int by giving it to f. In other words, a value of type T knows how to produce an int somehow. Well, we could eliminate the intermediate type X and just say:

T = int 

The universally quantified one is a little different.

T = ∀X { X a; int f(X); } 

This means: A value of type T can be given any type X, and it will produce a value a:X, and a function f:X->int no matter what X is. In other words: a consumer of values of type T can choose any type for X. And a producer of values of type T can't know anything at all about X, but it has to be able to produce a value a for any choice of X, and be able to turn such a value into an int.

Obviously implementing this type is impossible, because there is no program that can produce a value of every imaginable type. Unless you allow absurdities like null or bottoms.

Since an existential is a pair, an existential argument can be converted to a universal one via currying.

(∃b. F(b)) -> Int 

is the same as:

∀b. (F(b) -> Int) 

The former is a rank-2 existential. This leads to the following useful property:

Every existentially quantified type of rank n+1 is a universally quantified type of rank n.

There is a standard algorithm for turning existentials into universals, called Skolemization.

I think it makes sense to explain existential types together with universal types, since the two concepts are complementary, i.e. one is the "opposite" of the other.

I cannot answer every detail about existential types (such as giving an exact definition, list all possible uses, their relation to abstract data types, etc.) because I'm simply not knowledgeable enough for that. I'll demonstrate only (using Java) what this HaskellWiki article states to be the principal effect of existential types:

Existential types can be used for several different purposes. But what they do is to 'hide' a type variable on the right-hand side. Normally, any type variable appearing on the right must also appear on the left […]

Example set-up:

The following pseudo-code is not quite valid Java, even though it would be easy enough to fix that. In fact, that's exactly what I'm going to do in this answer!

class Tree<α> { α value; Tree<α> left; Tree<α> right; } int height(Tree<α> t) { return (t != null) ? 1 + max( height(t.left), height(t.right) ) : 0; } 

Let me briefly spell this out for you. We are defining…

• a recursive type Tree<α> which represents a node in a binary tree. Each node stores a value of some type α and has references to optional left and right subtrees of the same type.

• a function height which returns the furthest distance from any leaf node to the root node t.

Now, let's turn the above pseudo-code for height into proper Java syntax! (I'll keep on omitting some boilerplate for brevity's sake, such as object-orientation and accessibility modifiers.) I'm going to show two possible solutions.

1. Universal type solution:

The most obvious fix is to simply make height generic by introducing the type parameter α into its signature:

<α> int height(Tree<α> t) { return (t != null) ? 1 + max( height(t.left), height(t.right) ) : 0; } 

This would allow you to declare variables and create expressions of type α inside that function, if you wanted to. But...

2. Existential type solution:

If you look at our method's body, you will notice that we're not actually accessing, or working with, anything of type α! There are no expressions having that type, nor any variables declared with that type... so, why do we have to make height generic at all? Why can't we simply forget about α? As it turns out, we can:

int height(Tree<?> t) { return (t != null) ? 1 + max( height(t.left), height(t.right) ) : 0; } 

As I wrote at the very beginning of this answer, existential and universal types are complementary / dual in nature. Thus, if the universal type solution was to make height more generic, then we should expect that existential types have the opposite effect: making it less generic, namely by hiding/removing the type parameter α.

As a consequence, you can no longer refer to the type of t.value in this method nor manipulate any expressions of that type, because no identifier has been bound to it. (The ? wildcard is a special token, not an identifier that "captures" a type.) t.value has effectively become opaque; perhaps the only thing you can still do with it is type-cast it to Object.

Summary:

=========================================================== | universally existentially | quantified type quantified type ---------------------+------------------------------------- calling method | needs to know | yes no the type argument | ---------------------+------------------------------------- called method | can use / refer to | yes no the type argument | =====================+===================================== 

These are all good examples, but I choose to answer it a little bit differently. Recall from math, that ∀x. P(x) means "for all x's, I can prove that P(x)". In other words, it is a kind of function, you give me an x and I have a method to prove it for you.

In type theory, we are not talking about proofs, but of types. So in this space we mean "for any type X you give me, I will give you a specific type P". Now, since we don't give P much information about X besides the fact that it is a type, P can't do much with it, but there are some examples. P can create the type of "all pairs of the same type": P<X> = Pair<X, X> = (X, X). Or we can create the option type: P<X> = Option<X> = X | Nil, where Nil is the type of the null pointers. We can make a list out of it: List<X> = (X, List<X>) | Nil. Notice that the last one is recursive, values of List<X> are either pairs where the first element is an X and the second element is a List<X> or else it is a null pointer.

Now, in math ∃x. P(x) means "I can prove that there is a particular x such that P(x) is true". There may be many such x's, but to prove it, one is enough. Another way to think of it is that there must exist a non-empty set of evidence-and-proof pairs {(x, P(x))}.

Translated to type theory: A type in the family ∃X.P<X> is a type X and a corresponding type P<X>. Notice that while before we gave X to P, (so that we knew everything about X but P very little) that the opposite is true now. P<X> doesn't promise to give any information about X, just that there there is one, and that it is indeed a type.

How is this useful? Well, P could be a type that has a way of exposing its internal type X. An example would be an object which hides the internal representation of its state X. Though we have no way of directly manipulating it, we can observe its effect by poking at P. There could be many implementations of this type, but you could use all of these types no matter which particular one was chosen.

To directly answer your question:

With the universal type, uses of T must include the type parameter X. For example T<String> or T<Integer>. For the existential type uses of T do not include that type parameter because it is unknown or irrelevant - just use T (or in Java T<?>).

Further information:

Universal/abstract types and existential types are a duality of perspective between the consumer/client of an object/function and the producer/implementation of it. When one side sees a universal type the other sees an existential type.

In Java you can define a generic class:

public class MyClass<T> { // T is existential in here T whatever; public MyClass(T w) { this.whatever = w; } public static MyClass<?> secretMessage() { return new MyClass("bazzlebleeb"); } } // T is universal from out here MyClass<String> mc1 = new MyClass("foo"); MyClass<Integer> mc2 = new MyClass(123); MyClass<?> mc3 = MyClass.secretMessage(); 

• From the perspective of a client of MyClass, T is universal because you can substitute any type for T when you use that class and you must know the actual type of T whenever you use an instance of MyClass
• From the perspective of instance methods in MyClass itself, T is existential because it doesn't know the real type of T
• In Java, ? represents the existential type - thus when you are inside the class, T is basically ?. If you want to handle an instance of MyClass with T existential, you can declare MyClass<?> as in the secretMessage() example above.

Existential types are sometimes used to hide the implementation details of something, as discussed elsewhere. A Java version of this might look like:

public class ToDraw<T> { T obj; Function<Pair<T,Graphics>, Void> draw; ToDraw(T obj, Function<Pair<T,Graphics>, Void> static void draw(ToDraw<?> d, Graphics g) { d.draw.apply(new Pair(d.obj, g)); } } // Now you can put these in a list and draw them like so: List<ToDraw<?>> drawList = ... ; for(td in drawList) ToDraw.draw(td); 

It's a bit tricky to capture this properly because I'm pretending to be in some sort of functional programming language, which Java isn't. But the point here is that you are capturing some sort of state plus a list of functions that operate on that state and you don't know the real type of the state part, but the functions do since they were matched up with that type already.

Now, in Java all non-final non-primitive types are partly existential. This may sound strange, but because a variable declared as Object could potentially be a subclass of Object instead, you cannot declare the specific type, only "this type or a subclass". And so, objects are represented as a bit of state plus a list of functions that operate on that state - exactly which function to call is determined at runtime by lookup. This is very much like the use of existential types above where you have an existential state part and a function that operates on that state.

In statically typed programming languages without subtyping and casts, existential types allow one to manage lists of differently typed objects. A list of T<Int> cannot contain a T<Long>. However, a list of T<?> can contain any variation of T, allowing one to put many different types of data into the list and convert them all to an int (or do whatever operations are provided inside the data structure) on demand.

One can pretty much always convert a record with an existential type into a record without using closures. A closure is existentially typed, too, in that the free variables it is closed over are hidden from the caller. Thus a language that supports closures but not existential types can allow you to make closures that share the same hidden state that you would have put into the existential part of an object.

Seems I’m coming a bit late, but anyway, this document adds another view of what existential types are, although not specifically language-agnostic, it should be then fairly easier to understand existential types: Dijkstra, Atze - Essential Haskell (chapter 8).

The difference between a universally and existentially quantified type can be characterized by the following observation:

• The use of a value with a ∀ quantified type determines the type to choose for the instantiation of the quantified type variable. For example, the caller of the identity function “id :: ∀a.a → a” determines the type to choose for the type variable a for this particular application of id. For the function application “id 3” this type equals Int.
• The creation of a value with a ∃ quantified type determines, and hides, the type of the quantified type variable. For example, a creator of a “∃a.(a, a → Int)” may have constructed a value of that type from “(3, λx → x)”; another creator has constructed a value with the same type from “(’x’, λx → ord x)”. From a users point of view both values have the same type and are thus interchangeable. The value has a specific type chosen for type variable a, but we do not know which type, so this information can no longer be exploited. This value specific type information has been ‘forgotten’; we only know it exists.

An existential type is an opaque type.

Think of a file handle in Unix. You know its type is int, so you can easily forge it. You can, for instance, try to read from handle 43. If it so happens that the program has a file open with this particular handle, you'll read from it. Your code doesn't have to be malicious, just sloppy (e.g., the handle could be an uninitialized variable).

An existential type is hidden from your program. If fopen returned an existential type, all you could do with it is to use it with some library functions that accept this existential type. For instance, the following pseudo-code would compile:

let exfile = fopen("foo.txt"); // No type for exfile! read(exfile, buf, size); 

The interface "read" is declared as:

There exists a type T such that:

size_t read(T exfile, char* buf, size_t size); 

The variable exfile is not an int, not a char*, not a struct File—nothing you can express in the type system. You can't declare a variable whose type is unknown and you cannot cast, say, a pointer into that unknown type. The language won't let you.

A universal type exists for all values of the type parameter(s). An existential type exists only for values of the type parameter(s) that satisfy the constraints of the existential type.

For example in Scala one way to express an existential type is an abstract type which is constrained to some upper or lower bounds.

trait Existential { type Parameter <: Interface } 

Equivalently a constrained universal type is an existential type as in the following example.

trait Existential[Parameter <: Interface] 

Any use site can employ the Interface because any instantiable subtypes of Existential must define the type Parameter which must implement the Interface.

A degenerate case of an existential type in Scala is an abstract type which is never referred to and thus need not be defined by any subtype. This effectively has a shorthand notation of List[_] in Scala and List<?> in Java.

My answer was inspired by Martin Odersky's proposal to unify abstract and existential types. The accompanying slide aids understanding.

Research into abstract datatypes and information hiding brought existential types into programming languages. Making a datatype abstract hides info about that type, so a client of that type cannot abuse it. Say you've got a reference to an object... some languages allow you to cast that reference to a reference to bytes and do anything you want to that piece of memory. For purposes of guaranteeing behavior of a program, it's useful for a language to enforce that you only act on the reference to the object via the methods the designer of the object provides. You know the type exists, but nothing more.

See:

Abstract Types Have Existential Type, MITCHEL & PLOTKIN

http://theory.stanford.edu/~jcm/papers/mitch-plotkin-88.pdf

I created this diagram. I don't know if it's rigorous. But if it helps, I'm glad.

X and Y <=> forall Y, (A -> B -> Y) -> Y

We can name X and Y as R, R satisfies:

A -> B -> R

That means R can be created from both A and B.

forall Y, (A -> B -> Y) -> R -> Y

That means any other Y that can be created from both A and B can be created from R, too.

So, no matter how and what Y we want to create from A and B, we can store A and B into R temporality, then create Y from R. Such storing is called as currying.

we can also name R as product type.

X or Y <=> forall Y, (A -> Y) -> (B -> Y) -> Y

We can name X or Y as R, R satisfies:

A -> R

B -> R

That means R can be created from A or created from B.

forall Y, (A -> Y) -> (B -> Y) -> R -> Y

That means any other Y that can be created from A or created from B can be created from R, too.

So, no matter how and what Y we want to create from A or B, we can store A or B into R temporality, then create Y from R. Such storing is kind of type erasure.

we can also name R as sum type.

exist X, P(X) <=> forall Y, (forall X, P(X) -> Y) -> Y

We can name exist X, P(X) as R, R satisfies:

forall X, P(X) -> R

That means R can be created from any P(X).

forall Y, (forall X, P(X) -> Y) -> R -> Y

That means any other Y that can be created from any P(X) can be created from R, too.

So, no matter how and what Y we want to create from any P(X), we can store P(X) into R temporality, then create Y from R. Such storing is kind of type erasure, too.

we can also name R as existential type.
here is the existential type definition in Coq with an example:

Inductive my_ex_t (P: Type -> Type) := my_ex: forall (A: Type), (P A) -> my_ex_t P. Definition my_ex_eq1 {Y: Type} {P: Type -> Type}: (forall A: Type, (P A) -> Y) -> (my_ex_t P -> Y). intros temp_fun value. destruct value. exact (temp_fun A p). Defined. Definition my_ex_eq2 {Y: Type} {P: Type -> Type}: (my_ex_t P -> Y) -> (forall A: Type, (P A) -> Y). intros ex_fun A pa. apply ex_fun. apply (my_ex P A). apply pa. Defined. Definition add_1_fun_t (A: Type) := A -> A. Definition not_t (A: Type) := A -> bool. Definition not_0_nat: not_t nat. intros n. case n. - exact false. - intros _. exact true. Defined. Definition not_1_nat: not_t nat. intros n. case n. - exact true. - intros n'. case n'. + exact false. + intros _. exact true. Defined. Print S. Definition func_table_t(A: Type) := (prod (prod A (add_1_fun_t A)) (not_t A)). Definition add_check (A: Type) (func_table: func_table_t A): bool. destruct func_table. destruct p. apply n. apply a0. apply a. Defined. Definition func_table0 := pair (pair 0 S) not_0_nat. Definition func_table1 := pair (pair 0 S) not_1_nat. Compute (my_ex_eq1 add_check (my_ex func_table_t nat func_table0)). Compute (my_ex_eq1 add_check (my_ex func_table_t nat func_table1)).