What is an Existential Type?

Question

I read through the wikipedia entry on this. I gathered that they're called existential types because of the existential operator (∃). I'm not sure what the point of it is, though. What's the difference between

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

and

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

Answer 1

I think briefly: existential types are interfaces, and universal types are generics.

So for example, something like "ICollection" is effectively "there exists some concrete implementation type X where I can call .Length on X, but I don't know what type X it is". That's ICollection when you don't know if it's an Array or a List or whatnot. When you upcast a concrete type to an interface, you "forget" it's real type, and just know that there exists some concrete type with these interface properties.

Then something like "Stack<T>" is like "for any known T I can create a stack of it and call s.Push(T x)". For all T, I can stamp out a new instance of this thing.

That's kinda simplistic and not well-written (sorry), but it's the gist.

Answer 2

As I understand it's a math way to describe interfaces/abstract class.

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

For C# it would translate to a generic abstract type:

abstract class MyType<T>{
    private T a;

    public abstract int f(T x);
}

"Existential" just means that there is some type that obey to the rules defined here.

Answer 3

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

Answer 4

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.