Let’s explore existential types–these are types that are known to the component that produces them, but unknowable to the component that consumes them. Think about a hypothetical virtual machine that produces some compiled representation of some source code and it can then run the compiled code. In short, our VM compiles into type a that is unknown and unknowable to anything outside the VM; the only thing that the outside world knows is that it can take the value of type a and run it.

Scala

We’ll have a VirtualMachine, functions that create the different VMs and the compileAndRun function. Let’s begin with the VirtualMachine type:

trait VirtualMachine[A] {
  def compile: A
  def run: A => Unit
}

case class SimpleVirtualMachine[A](compile: A, run: A => Unit) 
  extends VirtualMachine[A]

We can now add the two functions that prepare the VM instances:

def helloWorldVM(s: String) = SimpleVirtualMachine(s, println)
def intVM(i: Int) = SimpleVirtualMachine(i, println)

So far, so good—let’s now add a function that can compile and run our VM code:

def compileAndRun(vm: VirtualMachine[A]) {
  vm.run(vm.compile)
}

It doesn’t compile: what type is A? We can sellotape it to compile by making compileAndRun polymorphic: compileAndRun[A](vm: VirtualMachine[A]), but that’d be wrong. The compileAndRun cannot chose the type A. It must take what is given to it in the VirtualMachine[A] and not “think” about it further.

All right. Let’s change it to

def compileAndRun(vm: VirtualMachine[Any]) { 
  vm.run(vm.compile)
}

Notice that the VirtualMachine is invariant in terms of its type argument A. This means that I cannot have

val hwvm: VirtualMachine[Any] = helloWorldVM("Test")
val intvm: VirtualMachine[Any] = intVM(42)

And thus, I cannot assign instance of VirtualMachine[Int] to VirtualMachine[Any]. And making the VirtualMachine‘s type parameter to covariant would be wrong. Existential types to the rescue. We change the compileAndRun to take instance of VirtualMachine[A] for some A.

def compileAndRun(vm: VirtualMachine[A] forSome {type A}) {
  vm.run(vm.compile)
}

And lo!—the compileAndRun function takes instance of VirtualMachine of A where A is indeed any type; calling compileAndRun(helloWorldVM("Yo!")) and compileAndRun(intVM(42)) compiles and works as expected.

In our “normal” Scala code, we would not write VirtualMachine[A] forSome {type A}, we’d simply say VirtualMachine[_], or, if we wanted to constrain the type somehow, we’d write VirtualMachine[_ <: SomeOtherType].

Haskell

Next, let's see how it looks like in Haskell. We define the VirtualMachine type with its constructor taking value of type a and a function from a to IO ().

{-# LANGUAGE ExistentialQuantification #-}

data VirtualMachine = forall a. MkVirtualMachine
    a               -- compile
    (a -> IO())     -- run

We then add an "implementation" of our VM that can execute some compiled version of its input:

{-# LANGUAGE ExistentialQuantification #-}

data VirtualMachine = forall a. MkVirtualMachine
    a               -- compile
    (a -> IO())     -- run

helloWorldVM :: String -> VirtualMachine
helloWorldVM source = MkVirtualMachine
  source                 -- we 'compile' the string into the same string
  putStrLn               -- we 'run' the instruction by showing it

Notice that the type a in the returned VirtualMachine is hidden from everywhere outside the helloWorldVM function. (Because it prepares the value a and the function that runs a.) We can create another VM, which operates on Ints:

{-# LANGUAGE ExistentialQuantification #-}

data VirtualMachine = forall a. MkVirtualMachine
    a               -- compile
    (a -> IO())     -- run

helloWorldVM :: String -> VirtualMachine
helloWorldVM source = MkVirtualMachine
  source                 -- we 'compile' the string into the same string
  putStrLn               -- we 'run' the instruction by showing it

intVM :: Int -> VirtualMachine
intVM i = MkVirtualMachine
  i
  (\i -> putStrLn (show i))

Finally, let's complete the source by dropping in the compileAndRun function. Again, this is the clever bit. The compileAndRun function operates on VirtualMachine values holding some type a, but it does not care what exactly this type a is.

{-# LANGUAGE ExistentialQuantification #-}
compileAndRun :: VirtualMachine -> IO ()
compileAndRun (MkVirtualMachine compile run) = run $ compile

compileAndRun (helloWorldVM "Hello, World")
compileAndRun (intVM 42)

Notice that the two functions helloWorldVM and intVM both translated our "source" to some internal representation of type a by compiling them and then provided a function that takes the value of the compiled type and runs it.

F#

I then wondered how such a thing would feel like in F#, but I could only get as far as the definitions of the types VirtualMachine and then the three functions.

type VirtualMachine< 'a> = SimpleVirtualMachine of ^a * (^a -> unit)

let helloWorldVM s = SimpleVirtualMachine(s, fun s -> printf "%A" s)
let intVM i = SimpleVirtualMachine(i, fun i -> printf "%d" i)

let compileAndRun (SimpleVirtualMachine (compile, run)) = compile |> run

F# does not worry about type variance, so---as far as I understand---the compileAndRun function essentially takes the first parameter as type obj and then pattern matches it. I can specify the type of its parameter as VirtualMachine<_>, which is simply VirtualMachine of anything, but without type variance. In other words, this is possible:

let m1: VirtualMachine<_> = helloWorldVM "Test"
let m2: VirtualMachine<_> = intVM 42

Which means that I can specify the type of the parameter of compileAndRun as

let compileAndRun (x: VirtualMachine<_>) = 
  match x with SimpleVirtualMachine (compile, run) -> compile |> run

Conclusion

Existential types allow you to write code that simply enforces their mere existence. Take the various forms of the compileAndRun function. We never said what type the VirtualMachine should use, we simply said that the type must exist. This means that you can have strongly & duck typed code---amazing!