Existential_currying.md

Quick explanation of why the "control inversion" trick in this explanation of existential types on StackOverflow is actually currying:

• the type of the original for-loop body was (∃B:VirtualMachine<B>) -> IO void
  • (where IO void represents that vm.run() had side-effects and a void return type)
• the type of VMHandler.handle() is ∀B:(VirtualMachine<B> -> IO void)

If you interpret an existential type as describing a pair of a type and a value, and interpret a universal type as describing a function from a type to a value (see footnote), then those can be interpreted as:

• the original for-loop body: (B, VirtualMachine<B>) -> IO void
• VMHandler.handle(): B -> VirtualMachine<B> -> IO void

Which is just currying!

This is also mentioned by the second-most voted answer, and explained at length by: http://iveselov.info/posts/2012-08-30-existential-types.html

Footnote: Universal type as function from type to value?

Right, that's what monomorphization means for C++ templates, Rust, Swift, Haskell: the compiler treats the generic function/class as a function from type to function/class, and for each type the generic is instantiated with, outputs a new copy of the function/class. Note that this all happens at compile-time, at run-time it's too late to monomorphize, so this cannot work for heterogenous lists of values with different types such as the List<VMWrapper> in the answer, which could potentially contain objects of many different classes all of which implement the VMWrapper interface. Instead you have to opt-out of monomorphization and use dynamic dispatch based on run-time type information, which in Rust you do with dyn, in Swift with any, in Haskell with ExistentialQuantification; in C++ you'd use virtual methods and subclassing instead of templates, because virtual methods are dynamically dispatched based on run-time type.

This complication doesn't exist in Java (the language used in the answer) because all methods are virtual/dynamically dispatched, there is no monomorphization in the first place to opt-out of. The Java compiler actually implements generics not by monomorphizing but by simply erasing type parameters:

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

The "function from type to value" is still there, to be clear, but it's 'evaluated' at run-time by dynamic dispatching, enabled by Java objects all having their type information at run-time; whereas those other languages do monomorphization and then erase type information at compile-time, unless you opt-out of monomorphization and thus opt-into preserving type information at run-time to do dynamic dispatch.