Universal types, and your type checker doesn't suck as much as you think
Universal types are very useful for performing generic programming, which allows you to use the same code over different types. For instance, the C++ STL (Standard Template Library) allows you to work on things like containers over any arbitrary type. You would surely not want to re-implement the logic for every concrete type that you use. Such a feature is known as parametric polymorphism. It is different from the other kind of polymorphism normally found in object-oriented languages that allows for overloading and run-time dispatch, which is known as ad-hoc polymorphism.
To formally introduce and discuss universal types, we work in the context of System F with universal (or polymorphic) types. System F is an extension of the simply-typed lambda calculus with universal quantification over types. The typing rules for System F are given below:
The first three rules are our old friends from the simply-typed lambda calculus, corresponding to variable typing, lambda abstraction, and lambda application. The rules
As an example, consider the empty context
Since we allow quantification over types, System F is a second-order lambda-calculus. In fact, we can go further and quantify over types of types, which is known as kinds. You can then say why not go further and take the type over kinds, and if repeat this process indefinitely you will actually achieve the language known as System
Languages from the ML family provides parametric polymorphism. However, it seems like not all is well. Consider the following piece of innocent OCaml code that simply defines the identity function and then tries to call it with two values of different types:
1
2
let id : 'a -> 'a = fun x -> x in
(id 0, id "hello")
Despite how we seemingly typed it to use any generic type variable, the compiler complains to us:
1
2
3
4
5
File "./ident.ml", line 2, characters 10-17:
2 | (id 0, id "hello")
^^^^^^^
Error: This expression has type string but an expression was expected of type
int
This is because OCaml uses the Hindley-Milner type inference algorithm in order to perform type reconstruction. From a high level point of view, it produces constraints on the types based on how they are used, and then tries to unify these constraints in the most general way possible. As such, it discovers both constraints
1
2
let id : 'a. 'a -> 'a = fun x -> x in
(id 0, id "hello")
Notice how the typing rule 'a. 'a -> 'a
closely resembles our type
Another way to achieve the same thing is by using explicit type parameters, which now really looks like our term in System F,
1
2
let id = fun (type a) (x : a) -> x in
(id 0, id "hello")
The first approach (polymorphic type annotations) is more idiomatic as explicit type parameters could cause issues when the function is recursive (see the following post if you want more information).
However, was this failure just a limitation of our type inference algorithm, and might there be a smarter way such that type inference in a language with first-class parametric polymorphism is possible? Interestingly enough, this was a very difficult question to answer, and was an open problem for around 20 years before Joe Wells proved that it is actually undecidable. Therefore, as a compromise, OCaml uses a weaker form of polymorphism known as let-polymorphism. Let-polymorphism essentially substitutes the binding into the resulting expression itself before typechecking, which allows each instance to be constrained independently of the others.
Related Posts: