Existential types

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!

This entry was posted in Jan's Blog and tagged , , , . Bookmark the permalink.

9 Responses to Existential types

  1. Matt R says:

    Does your (Scala) existential version of compileAndRun compile? I thought you had to capture the wildcard type in a polymorphic method before you could thread values of that type around.

    I’m not sure I’d agree that making compileAndRun polymorphic would be “wrong” — if you want to manipulate values of the generic type within the method, it seems a reasonable thing to give that type a name.

  2. Jan Machacek says:

    Yes, it does compile. When you say

    def compileAndRun(vm: VirtualMachine[_]), you’re saying VM of any type, as long as that type exists. It is not saying def compileAndRun(vm: VirtualMachine[Any]), which, because VirtualMachine is type invariant would only work with instances of VirtualMachine[Any]. The motivation is that the compileAndRun function takes VirtualMachine that internally operates on any type, but compileAndRun does not know and cannot know what type it is. All it knows is that it exists.

    This gives you flexibility–you can invent other VirtualMachines, parametrised by other types, and the compileAndRun won’t care. If you made the compileAndRun function polymorphic, then the compileAndRun function would know what type VirtualMachine operates on. (I know that I don’t do that in the code above, but you *could*. And the moment something can be done, someone will do it ;)

  3. Matt R says:

    I can only get it to compile using def compileAndRun(vm: VirtualMachine[A forSome { type A }]) rather than your version def compileAndRun(vm: VirtualMachine[A] forSome {type A}). Just a typo, I guess.

    Oddly, using “VirtualMachine[_]” also causes compilation errors (I’m using 2.9.2), even though it’s meant to desugar to the above.

    I hadn’t realised Scala was capable of letting you thread through values of the generic type, without needing to capture it as you would have to do in Java. That’s pretty convenient — a shame it doesn’t seem to work with the underscore syntax sugar!

    I would still argue that there’s nothing inherently wrong with making compileAndRun polymorphic in A — you say that compileAndRun would then know what type VirtualMachine operates on. Not exactly: all it really knows about it is that it exists, and that it can be referred to by the name “A” in that context. And given the relative clunkiness of the unsugared forSome syntax, I think the polymorphic version would be more readable.

  4. Jan Machacek says:

    D’oh! Thanks for spotting the typo. I think one of the main reasons for including this in Scala was to deal with Java generics!

    In most cases, though, you’ll want to avoid the clunky syntax–and given the body of compileAndRun, it’s not actually going to harm the generic-ness of compileAndRun. (I’ll experiment with 2.10 and report the results in the next post.)

  5. OlegYch says:

    Guys, I don’t think your scala will compile. See http://ideone.com/vPNyR (btw VirtualMachine[A forSome { type A }] is the same as VirtualMachine[Any] ).
    The only way for this to work is to use polymorphic function, and frankly i don’t see anything wrong with it.

    Oleg.

  6. Jan Machacek says:

    Let me just get over my manflu and I’ll get back to you.

    –J

  7. Matt R says:

    Oleg — thanks, yeah, you’re quite right, my version was also broken. I don’t think we’re the first to get a bit muddled by this, either: Minor revelation about Scala existential types ;-)

  8. mick says:

    What’s wrong with this compileAndRun[A](vm: VirtualMachine[A])?

  9. Jan Machacek says:

    Nothing–and this whole post needs tidying up. I have a follow-up prepared, showing off some of the Scala 2.10 compiler stuff.

Leave a Reply