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))

In case you have not seen this syntax before, the first pattern matches the empty tuple and the second all tuples with one or more elements.

The example poses a number of difficulties for a static type system. For instance, what type do the patterns have? Both of them should unify with items, but they do not even have the same length!

How can we get the types to agree, without sacrificing the additional information uncovered by pattern matching?

The answer is that we need two types per pattern: an abstract type to unify with the scrutinee (i.e. items) and another type local to each case. A type that is opaque to outsiders but is instantiated with a precise type locally is called an existential type.

Regular unification variables are allowed to unify with any other variable of the same kind, but local type variables cannot. If the local pattern types were allowed to leave the scope, they would meet in the scrutinee and cause a type error, since they have different sizes.

Existentials for closure environments

Closure conversion is a technique for eliminating free variables from functions by moving them to a record instead.

When performing closure conversion on a typed language, we may want the resulting form to be typed too. The record holding the free variables–the environment–will then need a type. But this can cause problems where the functions are used. Let’s look at an example:

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 perform closure conversion. We will need two environments, one for each function. 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 parameters added the code looks like this:

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

The lambda to the left expects an Env1 parameter, so its type is (Env1, Int) -> Int. The other function has type (Env2, Int) -> Int.

But now they do not have the same type, and suddenly the if expression does not type check! Both branches must agree.

The solution is to use the concrete type inside the function body but an abstract type outside it. This makes the environment opaque to callers. To them, both functions have type (T, Int) -> Int, for some abstract type T.

Conclusion

Even though the examples are very different, the underlying problem turned out to be the same in both cases.

Stefan