Higher rank polymorphism despite monomorphization

The conventional wisdom in type systems is that monomorphization and higher rank polymorphism are fundamentally incompatible. I think I have found a nice solution that is able to unify the two!

Let’s start at the beginning

There are two main strategies for compiling polymorphic functions: type erasure and monomorphization.

Type erasure is what languages like Haskell, OCaml and Java implement. With this strategy, every type internally has the same representation (usually a pointer to a heap allocation) and compilation just, well, erases types and compiles polymorphic functions exactly like monomorphic ones. While this has a few advantages, mostly that it is simple, compiles quickly and keeps executable sizes small, every value having the same representation makes it (mostly) impossible to have polymorphic functions that can act over unboxed values of different sizes, since calling conventions for these are different. Also, its performance is generally not fantastic, especially in languages with type classes that need to be compiled to indirect dictionaries, rather than directly inlining the type class methods.

Monomorphization, which low level languages like Rust and C++ implement, takes a very different approach. Here, the compiler compiles a separate instantiation for every type that a polymorphic function is used at. Because every type gets its own instantiation, each one of these can be specialized and, ideally, optimized for that specific type and calling convention. Compiling type classes this way boils down to picking the right instance for the type that the current instantiation is being compiled at.

The fundamental limitation of monomorphization now is that every instantiation of a polymorphic type has to be statically known, so that the compiler can pick the correct runtime implementation.

Higher rank polymorphism

Higher rank polymorphism allows functions to act over other polymorphic functions. For example, this function (f) takes another function (g) as a parameter, that has to be valid for any type a. This means that f is able to use g at type Int, as well as String.

f : (forall a. a -> a) -> (Int, String)
f(g) = (g(5), g("AAA"))

If you paid attention so far, you might see the issue already: There is no way for the compiler to statically know every instantiation of a higher rank polymorphic function. Even if it could, it would somehow have to pass f two copies of g and have f decide which one to use at runtime, which might not even be possible if f calls another higher rank polymorphic function.

The solution: restrict the types used in higher rank polymorphism

Higher rank polymorphism caused problems because it had to work for any type with any possible runtime representation.

If we restrict it to any type with the same representation, we can compile it with type erasure, just like we would in Haskell or OCaml!

Note that this does not significantly reduce the type system’s expressiveness, since any type can be wrapped in the same representation by boxing it (i.e. moving the value to the heap and keeping a pointer to it).

But how do we restrict types to “the same runtime representation”? We can take a page out of GHC’s playbook!

Kinds are calling conventions

In Haskell, types can have their own types, called kinds. E.g. Int has kind Type, whereas Maybe has kind Type -> Type and MonadState has kind Type -> (Type -> Type) -> Constraint.

But GHC also supports unboxed types (although it doesn’t support polymorphic functions ranging over every representation like our language, since it doesn’t monomorphize them).

The way that GHC allows these while keeping polymorphism is by encoding a type’s representation in its kind. Type from earlier is really just a kind synonym for TYPE LiftedRep, where LiftedRep represents any regular, lazy Haskell type that is represented by a pointer. By contrast, Int#, the type of unboxed integers has kind TYPE IntRep and Double# has kind TYPE DoubleRep.

This is what we need! In our hypothetical language then, a rank 1 polymorphic function definition with a top-level forall like this

f : forall a. a -> a
f(x) = x

is really just syntactic sugar for a representation polymorphic function (that will be monomorphized accordingly)

f : forall (r : RuntimeRep) (a : TYPE r). a -> a
f(x) = x

Higher rank polymorphic functions are only valid with monomorphic runtime representations. I.e. the following is fine and equivalent to what we had earlier without monomorphization

f : (forall (a : TYPE LiftedRep). a -> a) -> (Int, String)
f(g) = (g(5), g("AAA"))

But the following will be rejected because it is polymorphic over the representation of a.

f : (forall (r : RuntimeRep) (a : TYPE r). a -> a) -> (Int64, String)
f(g) = (g(5 : Int64), g("AAA"))