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 first pattern matches the empty tuple and the second all tuples with one or more elements.

This short example is enough to pose 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)

We also need a representation for the closures. They have two parts: an environment and a function. Let’s assume this representation:

record Closure[E](env: E, code: (E, Int) -> Int)

After transformation to explicit closures the example looks like this:

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

The free variables have been eliminated and the lambdas can be moved to the top level.

But now the if expression does not type check! The branches have different types after the transformation. The closure to the left expects an Env1 parameter, so its type is Closure[Env1]. The other has type Closure[Env2].

The solution is to use the concrete type inside the function body and an abstract type outside it. To the if statement, both functions will have type Closure[T], for some abstract type T (known as a skolem).

Conclusion

Even though the examples look very different, the underlying problems turned out to be similar.

Stefan