Polymorphism

Polymorphism

Polymorphism is a powerful tool many of us programmers take for granted nowadays. Simply put, it enables us to write code that’s generic over the types of the terms, therefore reducing the total amount of code that we have to write. The resulting code is by no means agnostic over the types but polymorphism allows us to instruct the compiler or interpreter to generate the specialized code for us. When talking about polymorphism, we usually refer to parametric polymorphism in particular. Terms like generics are often used to refer to polymorphism or a specific implementation of it but we don’t use them to avoid ambiguity.

Polymorphism in functions

The canonical example of polymorphism is the identity function . With a monomorphic type system, we’d have to define identity separately for each type:

int.id : Int -> Int
int.id = fun x : Int, x

char.id : Char -> Char
char.id = fun x : Char, x

bool.id : Bool -> Bool
bool.id = fun x : Bool, x

// ...

This feels like something the compiler or interpreter should be able to do for us, right? And in fact, many language implementations are able to do this. Below is an example of id in Haskell:

id :: a -> a
id x = x

example_int :: Int
example_int = id 42

example_bool :: Bool
example_bool = id True

Here, the compiler takes our polymorphic definition of id and specializes it for each type it gets called with, allowing us to write significantly less code.

Constrained polymorphism and Type Classes

When applying polymorphism, we rarely end up writing functions, such as id, that are generic over all types and more often than not, we want to define our functions for a specific subset of types, perhaps with some specific functionality. This is where the concept of type classes comes in. From the users perspective, type classes are a way to classify types based on their functionality and to constrain polymorphism to only work with a specific set of types.

all_equal :: Eq t => t -> t -> t -> Bool
all_equal a b c = a == b && b == c

Above, we’ve defined the function all_equal that is generic over all types t that implement the type class Eq and are therefore comparable with the == operator. In a similar fashion we can build other functions and APIs that work for multiple types as long as they behave in a specific way, while still utilizing the compiler to generate the repetitive code for us. In many cases, we can even stack these constraints, for instance, if we’d like for elements to be Eq and displayable as a string, we could change the type signature to (Eq t, Show t) => t -> t -> t -> Bool. We’ll dive into the specifics of type classes later on in this chapter

fn static_dispatch(t: impl ToString) -> String {
    t.to_string()
}

fn dynamic_dispatch(t: &dyn ToString) -> String {
    t.to_string()
}

pub fn main() {
    let s1 = static_dispatch(42);
    let s2 = static_dispatch("hello");

    println!("{s2} {s1}")
}

dynamic_dispatch:
        push    rbx
        mov     rbx, rdi
        call    qword ptr [rdx + 24] ; <- We're interested in this
        mov     rax, rbx
        pop     rbx
        ret

Polymorphism in

We created to teach how to explicitly reason about polymorphic code, i.e. code which is generic over one of the data types that it’s working on. To distinguish between type and term variables, term variables in must have a lowercase initial letter, whereas type variables must have an uppercase letter.

Polymorphism appears at both the term and the type level of code. At the term level, we can apply special kinds of functions to types. These special functions are called polymorphic abstractions (or polymorphic functions) and have a special type signature.

The traditional first example of a polymorphic function is the (polymorphic) identity function:

fun T : Type, fun x : T, x

It is composed of two abstractions which are different in nature. The outer fun binds a T : Type and is a polymorphic abstraction. The inner fun binds an x : T and is a regular term abstraction.

The grammatical structure of the polymorphic identity function is expressed in the following diagram:

As before, we have colored variable names blue and types purple.

Sorts

Polymorphism introduces another level to the language: sorts (also known as kinds).

Sorts are the “type” of types — the orange nodes in the above diagram. Just like how we refer to all integers by using the type Int, we refer to each type by using the sort Type — the only sort that we have in . However, it’s important to notice that even though we use the symbol : to denote both type and sort relations, they are completely different — one cannot speak about an integer variable x having a sort with x : Type.

We also like to say that polymorphic functions “quantify over” types rather than “abstract over”. The latter is reserved for regular functions that take in term-level values.

A common mistake is also to confuse polymorphic functions with type-level abstractions. The latter is from a more powerful type system, where types can be applied to types. In one cannot return a type from a function, so something like fun T : Type, List T is not supported. A function declared at type level is often called a type alias and many programming languages like Haskell and Rust have them.

In , because the only sort is Type, it can be omitted in polymorphic abstractions to make programming faster. The polymorphic identity can be shortened to fun T, fun x : T, x.

Applying Polymorphic Abstractions

Even though types are not terms, they can appear “next to” terms when we apply polymorphic abstractions to types. Let’s take the polymorphic identity function and apply it to Int

Int in itself is a base type, so it doesn’t contain type variables. A type variable is introduced when entering a polymorphic abstraction. The following tree shows a well-typed term where a type variable is applied to a polymorphic abstraction.

Type Context and Well-Formed Types

To motivate the concept of type context and well-formed types, we start with an example.

fun x : T, x

In the code given above, we define a function of type T -> T, where T is not any known type, rather a type variable. Surprisingly, the code doesn’t compile on its own — it needs to know something about T.

Suppose that the type T comes from a polymorphic abstraction. In the wider picture we can see that on the previous line a polymorphic abstraction introduces the type variable T:

fun T : Type,
fun x : T, x

To introduce a term or type variable means to add that variable to the context. This is happening within the type checker and not at runtime, so the context knows nothing about what the actual values are. Imagine that it’s just a list of pairs consisting of variable names and types.

With non-polymorphic abstractions, a term variable and its type are introduced for later reference when running into that variable name. Suppose that your task is to infer the type of the term

fun x : Int, x

First, you start with an empty context. Then as you enter the abstraction, you introduce x : Int, i.e. push ("x", Int) to the context. Now, you type check the body of the abstraction, i.e. x using the updated context, and you find the type of the variable x: Int. Finally, by combining the domain and codomain you return Int -> Int as the type of the term.

A very similar process happens during type checking polymorphic abstractions. To infer the type of the following term, we start from an empty context, however, this time the context also carries pairs of type variable names and sorts.

fun T : Type, fun x : T, x

First, the pair ("T", Type) is introduced to the context. Next, we run into the x and the type T, but before moving on, we need to verify that T is of “correct sort”, which is Type. We call a type of sort Type a well-formed type.

In a well-formed type must not contain free type variables.

Next, we technically infer the sort of T, which is like doing type inference, but for types instead of terms. Because T has sort Type in the context, we get back Type, and therefore T is well-formed.

From the type inference call of the inner abstraction we get back T -> T, which the type inference call of the polymorphic abstraction wraps in the a forall quantifier, which is the type used for polymorphic abstractions. The resulting type is forall T, T -> T.

We can diagrammatically depict the type inference as follows.

In the above diagram every solid arrow is recursively doing type inference on the subterm. The label on the arrow is the term/type variable introduced to the context. To recreate the context at a subterm in the tree, one joins all the variables introduced from the root term together.

Here’s what happens during type checking of the term fun T : Type, fun x : (forall X, T), x:

The interesting point here is that checking well-formedness of forall X, T involves introducing yet another type variable to the context.

Here are some common examples of polymorphic functions and their types:

As an example of a polymorphic function that quantifies over multiple type variables, we have the map function for lists:

map : forall A, forall B, (A -> B) -> [A] -> [B]
map = fun A, fun B, fun f : A -> B, fun xs : [A],
    lcase xs of
    | nil => nil B
    | cons x xs => (f x) :: map A B f xs

Notice that each forall in the type corresponds to a fun A or fun B in the term.

Polymorphic Equivalence Between Types

In the previous chapter we defined what an equivalence between types is and explored a couple of examples with concrete types. With knowledge of polymorphism, we can generalize some of the equivalences in the previous chapter to work across all types.

The equivalence

whose component functions are defined as

f : (Bool, Int) -> (Int, Bool)
f = fun p : (Bool, Int), (snd p, fst p)

g : (Int, Bool) -> (Bool, Int)
g = fun p : (Int, Bool), (snd p, fst p)

is “generic” over the types Bool and Int — no information about these types was used².

We can mathematically prove that if and are types, then , and give the component functions by “templating” in the types and . However, this is not ideal, because introducing the types would be done as part of the mathematics instead of in meaning that the code is not fit for evaluation.

Instead, we quantify over the type variables internally at the level of code in . To show the equivalence for any types , we define the following functions

f : forall A, forall B, (A, B) -> (B, A)
f = fun A, fun B, fun p : (A, B), (snd p, fst p)

g : forall A, forall B, (B, A) -> (A, B)
g = fun A, fun B, fun p : (B, A), (snd p, fst p)

Now, for all types and we have f A B : (A, B) -> (B, A) and g A B : (B, A) -> (A, B) which are the component function of .

By a similar argument as given in the previous chapter for , equivalence laws hold for f A B and g A B.

Compatibility Between Types

Let’s return to the topic of constrained polymorphism and think about how it could be implemented.

Consider the simple type class Add, which is implemented by types that provide a meaningful way of addition. Therefore, for each type that implements this, we’d require a function, or an API of sorts, that performs the addition. The signature of that function should be of form . Implementations of that API could be provided for Strings and Ints like shown below:

// API: function add : A -> A -> A
string.add : String -> String -> String
string.add = concat Char

int.add : Int -> Int -> Int
int.add = fun x : Int, fun y : Int, x + y

While doesn’t have type classes, we’re still able to mimic their core behavior to an extent. In our case, the type class constraint of Add, could mean that we constrain the function to only work for types for which there exists an instance of the add API. Another way to prove that this instance exists would be to pass it directly to the function using it.

With the established Add API, we can build arbitrarily complex functions that propagate it, such as muln below:

In a language with type classes, such as Haskell shown earlier, the instance passing is done a bit more implicitly. If our Add type class existed in Haskell, we could define the adder as Add t => t -> t -> t. This would result in the language providing us an instance of add that we’re allowed to use within the function, just like we manually did in .

You can think of the Add t => in Haskell almost like a regular arrow by thinking about Add t as t -> t -> t, so the adder would have type (t -> t -> t) -> t -> t -> t. Now, in the definition of the function, you can think that the argument left of => is bound with a parameter named add which means add : t -> t -> t is in scope. However, this is not the whole story, because, at the call-site, the type class mechanism needs to also find the type class instance that provides the concrete implementation of Add for t.

Our API is very implicit in the sense that it would be easy to misuse by providing a non-add function to it since all we require is A -> A -> A. Programming languages with type classes often make this easier to reason by allowing users to define interfaces and implementing them for types. This helps resolving ambiguities, since two interfaces are considered different even of their functions have the same signatures. Interfaces are a good way for hiding code behind an API, which helps reduce the complexity at hand — implementing muln becomes a lot easier when we can assume that add works with T correctly and according to the API.

In languages with type classes, this instance passing happens implicitly. If Add existed in Haskell, we could write adder : Add t => t -> t -> t, and the compiler would provide the appropriate add function automatically. Our manual approach is fragile — nothing stops us from passing a non-addition function since we only require the signature A -> A -> A. Type class systems solve this by letting users define named interfaces and explicitly implement them for types. Two interfaces are considered distinct even if their function signatures match, which eliminates ambiguity.

This also aids reasoning: when implementing muln, we can trust that add behaves correctly according to its interface, rather than worrying about what arbitrary function was passed in.

Footnotes