This chapter covers more advanced questions related to the limitations of polymorphic functions and types. There are some situations in OCaml where the type inferred by the type checker may be less generic than expected. Such non-genericity can stem either from interactions between side-effect and typing or the difficulties of implicit polymorphic recursion and higher-rank polymorphism.
This chapter details each of these situations and, if it is possible, how to recover genericity.
Maybe the most frequent examples of non-genericity derive from the interactions between polymorphic types and mutation. A simple example appears when typing the following expression
Since the type of None is 'a option and the function ref has type 'b -> 'b ref, a natural deduction for the type of store would be 'a option ref. However, the inferred type, '_weak1 option ref, is different. Type variables whose name starts with a _weak prefix like '_weak1 are weakly polymorphic type variables, sometimes shortened as weak type variables. A weak type variable is a placeholder for a single type that is currently unknown. Once the specific type t behind the placeholder type '_weak1 is known, all occurrences of '_weak1 will be replaced by t. For instance, we can define another option reference and store an int inside:
After storing an int inside another_store, the type of another_store has been updated from '_weak2 option ref to int option ref. This distinction between weakly and generic polymorphic type variable protects OCaml programs from unsoundness and runtime errors. To understand from where unsoundness might come, consider this simple function which swaps a value x with the value stored inside a store reference, if there is such value:
We can apply this function to our store
After these three swaps the stored value is 3. Everything is fine up to now. We can then try to swap 3 with a more interesting value, for instance a function:
At this point, the type checker rightfully complains that it is not possible to swap an integer and a function, and that an int should always be traded for another int. Furthermore, the type checker prevents us to change manually the type of the value stored by store:
Indeed, looking at the type of store, we see that the weak type '_weak1 has been replaced by the type int
Therefore, after placing an int in store, we cannot use it to store any value other than an int. More generally, weak types protect the program from undue mutation of values with a polymorphic type.
Moreover, weak types cannot appear in the signature of toplevel modules: types must be known at compilation time. Otherwise, different compilation units could replace the weak type with different and incompatible types. For this reason, compiling the following small piece of code
let option_ref = ref None
yields a compilation error
Error: The type of this expression, '_weak1 option ref,
contains type variables that cannot be generalized
To solve this error, it is enough to add an explicit type annotation to specify the type at declaration time:
let option_ref: int option ref = ref None
This is in any case a good practice for such global mutable variables. Otherwise, they will pick out the type of first use. If there is a mistake at this point, this can result in confusing type errors when later, correct uses are flagged as errors.
Identifying the exact context in which polymorphic types should be replaced by weak types in a modular way is a difficult question. Indeed the type system must handle the possibility that functions may hide persistent mutable states. For instance, the following function uses an internal reference to implement a delayed identity function
It would be unsound to apply this fake_id function to values with different types. The function fake_id is therefore rightfully assigned the type '_weak3 -> '_weak3 rather than 'a -> 'a. At the same time, it ought to be possible to use a local mutable state without impacting the type of a function.
To circumvent these dual difficulties, the type checker considers that any value returned by a function might rely on persistent mutable states behind the scene and should be given a weak type. This restriction on the type of mutable values and the results of function application is called the value restriction. Note that this value restriction is conservative: there are situations where the value restriction is too cautious and gives a weak type to a value that could be safely generalized to a polymorphic type:
Quite often, this happens when defining function using higher order function. To avoid this problem, a solution is to add an explicit argument to the function:
With this argument, id_again is seen as a function definition by the type checker and can therefore be generalized. This kind of manipulation is called eta-expansion in lambda calculus and is sometimes referred under this name.
There is another partial solution to the problem of unnecessary weak type, which is implemented directly within the type checker. Briefly, it is possible to prove that weak types that only appear as type parameters in covariant positions –also called positive positions– can be safely generalized to polymorphic types. For instance, the type 'a list is covariant in 'a:
Remark that the type inferred for empty is 'a list and not '_weak5 list that should have occurred with the value restriction since f () is a function application.
The value restriction combined with this generalization for covariant type parameters is called the relaxed value restriction.
Variance describes how type constructors behave with respect to subtyping. Consider for instance a pair of type x and xy with x a subtype of xy, denoted x :> xy:
As x is a subtype of xy, we can convert a value of type x to a value of type xy:
Similarly, if we have a value of type x list, we can convert it to a value of type xy list, since we could convert each element one by one:
In other words, x :> xy implies that x list :> xy list, therefore the type constructor 'a list is covariant (it preserves subtyping) in its parameter 'a.
Contrarily, if we have a function that can handle values of type xy
it can also handle values of type x:
Note that we can rewrite the type of f and f' as
In this case, we have x :> xy implies xy proc :> x proc. Notice that the second subtyping relation reverse the order of x and xy: the type constructor 'a proc is contravariant in its parameter 'a. More generally, the function type constructor 'a -> 'b is covariant in its return type 'b and contravariant in its argument type 'a.
A type constructor can also be invariant in some of its type parameters, neither covariant nor contravariant. A typical example is a reference:
If we were able to coerce x to the type xy ref as a variable xy, we could use xy to store the value `Y inside the reference and then use the x value to read this content as a value of type x, which would break the type system.
More generally, as soon as a type variable appears in a position describing mutable state it becomes invariant. As a corollary, covariant variables will never denote mutable locations and can be safely generalized. For a better description, interested readers can consult the original article by Jacques Garrigue on http://www.math.nagoya-u.ac.jp/~garrigue/papers/morepoly-long.pdf
Together, the relaxed value restriction and type parameter covariance help to avoid eta-expansion in many situations.
Moreover, when the type definitions are exposed, the type checker is able to infer variance information on its own and one can benefit from the relaxed value restriction even unknowingly. However, this is not the case anymore when defining new abstract types. As an illustration, we can define a module type collection as:
In this situation, when coercing the module List2 to the module type COLLECTION, the type checker forgets that 'a List2.t was covariant in 'a. Consequently, the relaxed value restriction does not apply anymore:
To keep the relaxed value restriction, we need to declare the abstract type 'a COLLECTION.t as covariant in 'a:
We then recover polymorphism:
The second major class of non-genericity is directly related to the problem of type inference for polymorphic functions. In some circumstances, the type inferred by OCaml might be not general enough to allow the definition of some recursive functions, in particular for recursive function acting on non-regular algebraic data type.
With a regular polymorphic algebraic data type, the type parameters of the type constructor are constant within the definition of the type. For instance, we can look at arbitrarily nested list defined as:
Note that the type constructor regular_nested always appears as 'a regular_nested in the definition above, with the same parameter 'a. Equipped with this type, one can compute a maximal depth with a classic recursive function
Non-regular recursive algebraic data types correspond to polymorphic algebraic data types whose parameter types vary between the left and right side of the type definition. For instance, it might be interesting to define a datatype that ensures that all lists are nested at the same depth:
Intuitively, a value of type 'a nested is a list of list …of list of elements a with k nested list. We can then adapt the maximal_depth function defined on regular_depth into a depth function that computes this k. As a first try, we may define
The type error here comes from the fact that during the definition of depth, the type checker first assigns to depth the type 'a -> 'b . When typing the pattern matching, 'a -> 'b becomes 'a nested -> 'b, then 'a nested -> int once the List branch is typed. However, when typing the application depth n in the Nested branch, the type checker encounters a problem: depth n is applied to 'a list nested, it must therefore have the type 'a list nested -> 'b. Unifying this constraint with the previous one leads to the impossible constraint 'a list nested = 'a nested. In other words, within its definition, the recursive function depth is applied to values of type 'a t with different types 'a due to the non-regularity of the type constructor nested. This creates a problem because the type checker had introduced a new type variable 'a only at the definition of the function depth whereas, here, we need a different type variable for every application of the function depth.
The solution of this conundrum is to use an explicitly polymorphic type annotation for the type 'a:
In the type of depth, 'a.'a nested -> int, the type variable 'a is universally quantified. In other words, 'a.'a nested -> int reads as “for all type 'a, depth maps 'a nested values to integers”. Whereas the standard type 'a nested -> int can be interpreted as “let be a type variable 'a, then depth maps 'a nested values to integers”. There are two major differences with these two type expressions. First, the explicit polymorphic annotation indicates to the type checker that it needs to introduce a new type variable every times the function depth is applied. This solves our problem with the definition of the function depth.
Second, it also notifies the type checker that the type of the function should be polymorphic. Indeed, without explicit polymorphic type annotation, the following type annotation is perfectly valid
since 'a,'b and 'c denote type variables that may or may not be polymorphic. Whereas, it is an error to unify an explicitly polymorphic type with a non-polymorphic type:
An important remark here is that it is not needed to explicit fully the type of depth: it is sufficient to add annotations only for the universally quantified type variables:
With explicit polymorphic annotations, it becomes possible to implement any recursive function that depends only on the structure of the nested lists and not on the type of the elements. For instance, a more complex example would be to compute the total number of elements of the nested lists:
Similarly, it may be necessary to use more than one explicitly polymorphic type variables, like for computing the nested list of list lengths of the nested list:
Explicit polymorphic annotations are however not sufficient to cover all the cases where the inferred type of a function is less general than expected. A similar problem arises when using polymorphic functions as arguments of higher-order functions. For instance, we may want to compute the average depth or length of two nested lists:
It would be natural to factorize these two definitions as:
However, the type of average len is less generic than the type of average_len, since it requires the type of the first and second argument to be the same:
As previously with polymorphic recursion, the problem stems from the fact that type variables are introduced only at the start of the let definitions. When we compute both f x and f y, the type of x and y are unified together. To avoid this unification, we need to indicate to the type checker that f is polymorphic in its first argument. In some sense, we would want average to have type
val average: ('a. 'a nested -> int) -> 'a nested -> 'b nested -> int
Note that this syntax is not valid within OCaml: average has an universally quantified type 'a inside the type of one of its argument whereas for polymorphic recursion the universally quantified type was introduced before the rest of the type. This position of the universally quantified type means that average is a second-rank polymorphic function. This kind of higher-rank functions is not directly supported by OCaml: type inference for second-rank polymorphic function and beyond is undecidable; therefore using this kind of higher-rank functions requires to handle manually these universally quantified types.
In OCaml, there are two ways to introduce this kind of explicit universally quantified types: universally quantified record fields,
and universally quantified object methods:
To solve our problem, we can therefore use either the record solution:
or the object one: