An Introduction to Existential Types

Parametric polymorphism is now widely known in the programming community (often by the alternate name generics). They allow one to create types parameterized by another type (e.g. a generic list type), along with functions that work on any type (e.g. the functional programming mainstays map, filter, and reduce ). You may have also heard them called universal types. This last nomenclature comes from logic.

If you’re familiar with some math or logic, you may rightly wonder whether universal quantification’s twin sibling — existential quantification — also appears in programming. Well, the title already spoiled that. Existential types do, ahem, exist, though they’re less well known, and they are a part of very few languages, even the more academic ones. In fact, they don’t even have a wikipedia article! It is this lack of materials that compelled me to write an introductory article on the topic. Here I hope at a minimum to show you what they are, and hopefully to convince you why they might be useful.

Let’s start with the what. Existential types allow us to create abstract data types: stacks, queues, maps, heaps, etc. More generally, they allow one to create any new type they like that doesn’t already exist in the base language, in terms of other types. This allows programmers (especially library authors) to create the type that best fits their use cases, instead of relying on whatever types are built into the language.

For the following examples, I’m going to start out with idealized pseudo-code, and then show some examples in a real language, OCaml, near the end. If you’re familiar with functional programming in the vein of ML or Haskell, you should be able to follow right along. Even if you’re not, I’ll try to explain what’s going on as best as I without this turning into a programming tutorial (I think the concepts are more important here).

As a first example, let’s say we’re working in some language without natural numbers. This actually isn’t too far-fetched, as most languages only provide fixed-width integers, not bona-fide natural numbers. We could use int, but we want more safety: we don’t want to be able to do non-sensical operations on naturals, such as division. As such, we want to define our own natural numbers in this language. How would we go about that?

Natural numbers are defined by two rules (or axioms): there exists a natural number called zero, and if n is a natural number, then succ(n) is a natural number (succ is short for successor). For example, succ(succ(0)) is the number normally written 2 in Arabic numerals.

Here is the type of natural numbers using existential:

type natNums = exists t. { zero: t, succ: t -> t }

This will look funny at first, but let’s go over it piece-by-piece. The right-hand side is the actual existential type (the left-hand side just assigns a name to it). It says that there exists some specific but hidden type t, along with a record containing two fields: zero, which creates a value of type t, and succ, a function which takes in a t and returns a t. tis called the implementation type; it doesn’t matter what the actual type of t is, as long as we can use it to implement the two operations specified. This gives us freedom to swap out implementations if need be. It also lets us hide potentially ugly (but efficient) implementation and provide a clean interface over.

Here’s one way to implement it:

let myNat: natNums = pack (type nat = Zero | Succ nat) with { zero: Zero, succ: fn n -> Succ n }

The pack and with are just keywords that hopefully suggest what is happening: we are packing an implementation type with a record that makes use of it. fn is the notation I’m using for function definition. We’re using type nat = Zero | Succ nat as our implementation type, which we’ve also simultaneously defined. Now, admittedly, using the existential interface is no more straightforward than using the type nat directly. But keep in mind that a) this is only a simple example and b) natis actually quite inefficient (it’s essentially unary), so in a real implementation we would want to make use of a smarter implementation type.

In fact, let’s create another implementation of natural numbers, but this time using the builtin int type for efficiency:

let intNat: natNums = pack (type nat = int) with { zero: 0, succ: fn n -> n + 1}

This type will naturally be much faster to use, but it’s still “safe”. For example, since the type t is abstract, we can’t use it for subtraction or division, even though the backing type is int, as that’s hidden by the interface.

Finally, let’s use the type we’ve created above. We can use either implementation — here we’ll use intNat. Then we could write:

intNat.succ(intNat.succ(intNat.zero))

It’s time to crack the champagne, because we’ve just created the number 2!

If you’re still with me, it’s time we move on to a more practical example. The reason I wanted to start with the natural number example is because it only makes use of simple types, whereas the following example will use type constructors, i.e. generics.

Let’s create a type for stacks. What operations do we need? We need push and pop, of course, but we also need the ability to create an empty stack, so we have a base to work with. A more complete implementation would include further operations, such as peek and reverse.

Here’s the type we’ll use:

type stack = exists 'a t. { emp: 'a t, push: 'a t * 'a -> 'a t, pop: 'a t -> 'a t * 'a option }

Here, I’m specifying that the hidden type is in fact a type constructor t parameterized by another type 'a. This means that the t is still hidden, but any 'a can be supplied by the caller, to get e.g. a stack of integers, a stack of strings, or even a stack of stacks of strings! Also note that pop returns bothed the popped element and the remainder of the stack.

Here’s a stupid-simple example implementation:

let listStack: stack = pack 'a list as {emp: [], push: fn (elem, stack) => elem::stack, pop: fn stack => case stack of x::xs -> (xs, Some x) | nil ->  (nil, None)

Here, our implementation type is 'a list (which I’m assuming for brevity is built into the language). Push is simply cons/append, and pop extracts the head of the list through pattern-matching.

To create the stack equivalent of “Hello, world!”, we could write:

listStack.push ("world", listStack.push ("Hello", listStack.emp))

Now, why would anyone want to do this? Why are these types and constructs useful? Well, the astute reader may have noticed that they look suspiciously like objects. If you did, I award you one (existent but hidden) cookie. The fact is that existential types and classes are both ways to define abstract data types, as I mentioned earlier.

But there are a few key differences. Classes are existential types bundled up with several other programming-language concepts that ought to be separate. It depends on the language, but in general, classes are a combination of:

1. Abstract data types: define new types that don’t exist in the core language
2. Implementation reuse through inheritance
3. Subtype polymorphism, though either inheritance or interfaces
4. Modules, i.e. a way to separate and structure code
5. Records aka products types aka structs: that is, a bundle of named values
6. Open recursion and self reference: every method of an object has access — either implicitly (e.g. Java) or explicitly (e.g. Python) — to the object itself, which is often called this or self

There’s nothing wrong with any of these ideas. They are all useful tools in the programming toolkit. But tying them all up together doesn’t provide any benefit in my eyes, and separating them opens up new opportunity. This is akin to how many languages combine the definition of a function with the naming of a function. But often we just want to define a function without naming it (anonymous functions are quite useful in functional programming), and many languages now allow this. Analogously, sometimes one would like to use abstract data types, and just abstract types, without all the other baggage.

Anyway, now let’s get to real-world programming. What languages implement existential types (in a form similar to that given here, and not as objects)? The ML family does (including SML and OCaml). The ML module system allows us to create existential types, but “one level up”. This means that existentials in ML are not first-class: namely, they can’t be passed to or returned from functions. However, there are in fact also functions “one level up” in ML called functors (no relation to the concept from category theory) that do allow such manipulation.

Below, I’ll write out the existential type for a stack as an OCaml signature:

module type STACK = sig
  type 'a t
  val emp: 'a t
  val push: 'a * 'a t -> 'a t
  val pop: 'a t -> 'a option
end

And an implementation:

module Stack: STACK = struct
  type 'a t = 'a list
  let emp = []
  let push (elem, stack) = elem::stack
  let pop stack = case stack of x::_ => Some x | [] => None
end

Note that in ML, modules not only allow the creation of existential types, but also perform the usual function of organizing code into hierarchical namespaces.

And actually, I lied before: while SML doesn’t support first-class modules, OCaml does. This means we can use existenials in much the same way I have laid out in this post. To create a first-class module from a normal module, we would write:

let my_stack = (module Stack: STACK)

I think I’ll end it there, though, as I don’t want this post to start getting into the details of OCaml.

I hope you’ve found existential types as interesting as I do. It’s a shame we don’t get them in this form in many languages. But it only took something like 30 years for generics to make it from academia to mainstream programming, so I’m hopeful that by the time robots have taken over the world, they’ll be using existentials to write the code that enslaves humanity.