What is an existential type?

Question

I read through the Wikipedia article Existential types. 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

When someone defines a universal type ∀X they're saying: You can plug in whatever type you want, I don't need to know anything about the type to do my job, I'll only refer to it opaquely as X.

When someone defines an existential type ∃X they're saying: I'll use whatever type I want here; you won't know anything about the type, so you can only refer to it opaquely as X.

Universal types let you write things like:

void copy<T>(List<T> source, List<T> dest) {
   ...
}

The copy function has no idea what T will actually be, but it doesn't need to know.

Existential types would let you write things like:

interface VirtualMachine<B> {
   B compile(String source);
   void run(B bytecode);
}

// Now, if you had a list of VMs you wanted to run on the same input:
void runAllCompilers(List<∃B:VirtualMachine<B>> vms, String source) {
   for (∃B:VirtualMachine<B> vm : vms) {
      B bytecode = vm.compile(source);
      vm.run(bytecode);
   }
}

Each virtual machine implementation in the list can have a different bytecode type. The runAllCompilers function has no idea what the bytecode type is, but it doesn't need to; all it does is relay the bytecode from VirtualMachine.compile to VirtualMachine.run.

Java type wildcards (ex: List<?>) are a very limited form of existential types.

Update: Forgot to mention that you can sort of simulate existential types with universal types. First, wrap your universal type to hide the type parameter. Second, invert control (this effectively swaps the "you" and "I" part in the definitions above, which is the primary difference between existentials and universals).

// A wrapper that hides the type parameter 'B'
interface VMWrapper {
   void unwrap(VMHandler handler);
}

// A callback (control inversion)
interface VMHandler {
   <B> void handle(VirtualMachine<B> vm);
}

Now, we can have the VMWrapper call our own VMHandler which has a universally-typed handle function. The net effect is the same, our code has to treat B as opaque.

void runWithAll(List<VMWrapper> vms, final String input)
{
   for (VMWrapper vm : vms) {
      vm.unwrap(new VMHandler() {
         public <B> void handle(VirtualMachine<B> vm) {
            B bytecode = vm.compile(input);
            vm.run(bytecode);
         }
      });
   }
}

An example VM implementation:

class MyVM implements VirtualMachine<byte[]>, VMWrapper {
   public byte[] compile(String input) {
      return null; // TODO: somehow compile the input
   }
   public void run(byte[] bytecode) {
      // TODO: Somehow evaluate 'bytecode'
   }
   public void unwrap(VMHandler handler) {
      handler.handle(this);
   }
}