What is an existential type?

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.

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.

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.