Existential Types in Practical Terms

It turns out that pattern matching on Python-style tuples requires existential types. This is the second time I encounter them, so I figured it is a good opportunity to show how they arise in practise.

Existentials in match patterns

Let’s say you want to apply a function to all items in a tuple, and you want to do it using recursion instead of a for loop. Something like this:

def map(fun, items):
    match items:
        case Tuple():
            return Tuple()

        case Tuple(first, *rest):
            return Tuple(fun(first), *map(fun, rest))

The patterns are meant to match the empty tuple and tuples with one or more elements.

This simple example is enough to present a number of difficulties for a static type system. For instance, what is the type of first in the second case pattern? We don’t know anything about it, and outside the match case the value isn’t even guaranteed to exist!

The combination of being unknown and local (confined to a scope) makes it existential.

Now you may be thinking, how is this different from a unification variable? After all, we make up fresh variables for unknown types all the time in Hindley Milner.

The difference is that those variables can unify with any other variable of the same kind, but first’s type variable cannot. It is not allowed to appear inside items’ type, for instance. If it could unify with anything, it would be universal.

Existentials for closure environments

Closure conversion is a technique for eliminating free variables from functions by moving them to a record instead, called its environment. When performing closure conversion on a typed language, we usually want the output to also be typed. That means the record holding the free variables–the environment–must have a specific type. That is unproblematic inside the original function body, but causes problems where the function is used. Take this code for instance:

let b = 1
let fun = (lambda a: a + 1) if condition else (lambda a: a + b)

Both sides of the if expression are functions from Int to Int, so we can safely assign fun the type Int -> Int. So far everything is great.

Now let’s add environments. The first lambda does not have any free variables, so its environment is an empty record. The other has a field for b.

record Env1()
record Env2(b: Int)

With env parameters added:

let b = 1
let fun = (lambda env, a: a + 1) if condition else (lambda env, a: a + env.b)

Unfortunately, the lambdas no longer have the same type. One has type (Env1, Int) -> Int and the other (Env2, Int) -> Int. Consequently, the if expression is now ill-typed. Oh no!

The same problem occurs for calls. We want function calls that were well-typed before closure conversion to remain so.

The solution is to use the concrete type inside the function body but an abstract type outside it. This makes the environment opaque to client code–it will look the same everywhere regardless of which particular record was created. To outsiders, both functions now have type (T, Int) -> Int, for some existential type T.

Stefan