Chapter 5 Polymorphism and its limitations

This chapter covers more advanced questions related to thelimitations of polymorphic functions and types. There are some situationsin OCaml where the type inferred by the type checker may be less genericthan expected. Such non-genericity can stem either from interactionsbetween side-effect and typing or the difficulties of implicit polymorphicrecursion and higher-rank polymorphism.

This chapter details each of these situations and, if it is possible,how to recover genericity.

5.1 Weak polymorphism and mutation

5.1.1 Weakly polymorphic types

Maybe the most frequent examples of non-genericity derive from theinteractions between polymorphic types and mutation. A simple exampleappears when typing the following expression

  1.  let store = ref None ;;
  2. val store : '_weak1 option ref = {contents = None}

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, isdifferent. Type variables whose name starts with a _weak prefix like'_weak1 are weakly polymorphic type variables, sometimes shortened asweak type variables.A weak type variable is a placeholder for a single type that is currentlyunknown. Once the specific type t behind the placeholder type '_weak1is known, all occurrences of '_weak1 will be replaced by t. For instance,we can define another option reference and store an int inside:

  1.  let another_store = ref None ;;
  2. val another_store : '_weak2 option ref = {contents = None}
  1.  another_store := Some 0;
  2.   another_store ;;
  3. - : int option ref = {contents = Some 0}

After storing an int inside another_store, the type of another_store hasbeen updated from '_weak2 option ref to int option ref.This distinction between weakly and generic polymorphic type variable protectsOCaml programs from unsoundness and runtime errors. To understand from whereunsoundness might come, consider this simple function which swaps a value xwith the value stored inside a store reference, if there is such value:

  1.  let swap store x = match !store with
  2.     | None -> store := Some x; x
  3.     | Some y -> store := Some x; y;;
  4. val swap : 'a option ref -> 'a -> 'a = <fun>

We can apply this function to our store

  1.  let one = swap store 1
  2.   let one_again = swap store 2
  3.   let two = swap store 3;;
  4. val one : int = 1
  5. val one_again : int = 1
  6. val two : int = 2

After these three swaps the stored value is 3. Everything is fine up tonow. We can then try to swap 3 with a more interesting value, forinstance a function:

  1.  let error = swap store (fun x -> x);;
  2. Error: This expression should not be a function, the expected type is int

At this point, the type checker rightfully complains that it is notpossible to swap an integer and a function, and that an int should alwaysbe traded for another int. Furthermore, the type checker prevents us tochange manually the type of the value stored by store:

  1.  store := Some (fun x -> x);;
  2. Error: This expression should not be a function, the expected type is int

Indeed, looking at the type of store, we see that the weak type '_weak1 hasbeen replaced by the type int

  1.  store;;
  2. - : int option ref = {contents = Some 3}

Therefore, after placing an int in store, we cannot use it to store anyvalue other than an int. More generally, weak types protect the program fromundue 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 compilationunits could replace the weak type with different and incompatible types.For this reason, compiling the following small piece of code

  1. let option_ref = ref None

yields a compilation error

  1. Error: The type of this expression, '_weak1 option ref,
  2.        contains type variables that cannot be generalized

To solve this error, it is enough to add an explicit type annotation tospecify the type at declaration time:

  1. 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 mistakeat this point, this can result in confusing type errors when later, correctuses are flagged as errors.

5.1.2 The value restriction

Identifying the exact context in which polymorphic types should bereplaced by weak types in a modular way is a difficult question. Indeedthe type system must handle the possibility that functions may hide persistentmutable states. For instance, the following function uses an internal referenceto implement a delayed identity function

  1.  let make_fake_id () =
  2.     let store = ref None in
  3.     fun x -> swap store x ;;
  4. val make_fake_id : unit -> 'a -> 'a = <fun>
  1.  let fake_id = make_fake_id();;
  2. val fake_id : '_weak3 -> '_weak3 = <fun>

It would be unsound to apply this fake_id function to values with differenttypes. The function fake_id is therefore rightfully assigned the type'_weak3 -> '_weak3 rather than 'a -> 'a. At the same time, it ought tobe possible to use a local mutable state without impacting the type of afunction.

To circumvent these dual difficulties, the type checker considers that any valuereturned by a function might rely on persistent mutable states behind the sceneand should be given a weak type. This restriction on the type of mutablevalues and the results of function application is called the value restriction.Note that this value restriction is conservative: there are situations where thevalue restriction is too cautious and gives a weak type to a value that could besafely generalized to a polymorphic type:

  1.  let not_id = (fun x -> x) (fun x -> x);;
  2. val not_id : '_weak4 -> '_weak4 = <fun>

Quite often, this happens when defining function using higher order function.To avoid this problem, a solution is to add an explicit argument to thefunction:

  1.  let id_again = fun x -> (fun x -> x) (fun x -> x) x;;
  2. val id_again : 'a -> 'a = <fun>

With this argument, id_again is seen as a function definition by the typechecker and can therefore be generalized. This kind of manipulation is calledeta-expansion in lambda calculus and is sometimes referred under this name.

5.1.3 The relaxed value restriction

There is another partial solution to the problem of unnecessary weak type,which is implemented directly within the type checker. Briefly, it is possibleto prove that weak types that only appear as type parameters in covariantpositions –also called positive positions– can be safely generalized topolymorphic types. For instance, the type 'a list is covariant in 'a:

  1.    let f () = [];;
  2. val f : unit -> 'a list = <fun>
  1.    let empty = f ();;
  2. val empty : 'a list = []

Remark that the type inferred for empty is 'a list and not '_weak5 listthat should have occurred with the value restriction since f () is afunction application.

The value restriction combined with this generalization for covariant typeparameters is called the relaxed value restriction.

5.1.4 Variance and 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:

  1.    type x = [ `X ];;
  2. type x = [ `X ]
  1.    type xy = [ `X | `Y ];;
  2. type xy = [ `X | `Y ]

As x is a subtype of xy, we can convert a value of type xto a value of type xy:

  1.    let x:x = `X;;
  2. val x : x = `X
  1.    let x' = ( x :> xy);;
  2. val x' : xy = `X

Similarly, if we have a value of type x list, we can convert it to a valueof type xy list, since we could convert each element one by one:

  1.    let l:x list = [`X; `X];;
  2. val l : x list = [`X; `X]
  1.    let l' = ( l :> xy list);;
  2. val l' : xy list = [`X; `X]

In other words, x :> xy implies that x list :> xy list, thereforethe 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

  1.    let f: xy -> unit = function
  2.     | `X -> ()
  3.     | `Y -> ();;
  4. val f : xy -> unit = <fun>

it can also handle values of type x:

  1.    let f' = (f :> x -> unit);;
  2. val f' : x -> unit = <fun>

Note that we can rewrite the type of f and f' as

  1.    type 'a proc = 'a -> unit
  2.     let f' = (f: xy proc :> x proc);;
  3. type 'a proc = 'a -> unit
  4. val f' : x proc = <fun>

In this case, we have x :> xy implies xy proc :> x proc. Noticethat 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 inits 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:

  1.    let x: x ref = ref `X;;
  2. val x : x ref = {contents = `X}

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 usethe 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 describingmutable state it becomes invariant. As a corollary, covariant variables willnever denote mutable locations and can be safely generalized.For a better description, interested readers can consult the originalarticle by Jacques Garrigue onhttp://www.math.nagoya-u.ac.jp/~garrigue/papers/morepoly-long.pdf

Together, the relaxed value restriction and type parameter covariancehelp to avoid eta-expansion in many situations.

5.1.5 Abstract data types

Moreover, when the type definitions are exposed, the type checkeris able to infer variance information on its own and one can benefit fromthe relaxed value restriction even unknowingly. However, this is not the caseanymore when defining new abstract types. As an illustration, we can define amodule type collection as:

  1.  module type COLLECTION = sig
  2.     type 'a t
  3.     val empty: unit -> 'a t
  4.   end
  6.   module Implementation = struct
  7.     type 'a t = 'a list
  8.     let empty ()= []
  9.   end;;
  10. module type COLLECTION = sig type 'a t val empty : unit -> 'a t end
  11. module Implementation :
  12.   sig type 'a t = 'a list val empty : unit -> 'a list end
  1.  module List2: COLLECTION = Implementation;;
  2. module List2 : COLLECTION

In this situation, when coercing the module List2 to the module typeCOLLECTION, the type checker forgets that 'a List2.t was covariantin 'a. Consequently, the relaxed value restriction does not apply anymore:

  1.    List2.empty ();;
  2. - : '_weak5 List2.t = <abstr>

To keep the relaxed value restriction, we need to declare the abstract type'a COLLECTION.t as covariant in 'a:

  1.  module type COLLECTION = sig
  2.     type +'a t
  3.     val empty: unit -> 'a t
  4.   end
  6.   module List2: COLLECTION = Implementation;;
  7. module type COLLECTION = sig type +'a t val empty : unit -> 'a t end
  8. module List2 : COLLECTION

We then recover polymorphism:

  1.    List2.empty ();;
  2. - : 'a List2.t = <abstr>

5.2 Polymorphic recursion

The second major class of non-genericity is directly related to the problemof type inference for polymorphic functions. In some circumstances, the typeinferred by OCaml might be not general enough to allow the definition ofsome recursive functions, in particular for recursive function acting onnon-regular algebraic data type.

With a regular polymorphic algebraic data type, the type parameters ofthe type constructor are constant within the definition of the type. Forinstance, we can look at arbitrarily nested list defined as:

  1.    type 'a regular_nested = List of 'a list | Nested of 'a regular_nested list
  2.     let l = Nested[ List [1]; Nested [List[2;3]]; Nested[Nested[]] ];;
  3. type 'a regular_nested = List of 'a list | Nested of 'a regular_nested list
  4. val l : int regular_nested =
  5.   Nested [List [1]; Nested [List [2; 3]]; Nested [Nested []]]

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 witha classic recursive function

  1.    let rec maximal_depth = function
  2.     | List _ -> 1
  3.     | Nested [] -> 0
  4.     | Nested (a::q) -> 1 + max (maximal_depth a) (maximal_depth (Nested q));;
  5. val maximal_depth : 'a regular_nested -> int = <fun>

Non-regular recursive algebraic data types correspond to polymorphic algebraicdata types whose parameter types vary between the left and right side ofthe type definition. For instance, it might be interesting to define a datatypethat ensures that all lists are nested at the same depth:

  1.    type 'a nested = List of 'a list | Nested of 'a list nested;;
  2. type 'a nested = List of 'a list | Nested of 'a list nested

Intuitively, a value of type 'a nested is a list of list …of list ofelements a with k nested list. We can then adapt the maximal_depthfunction defined on regular_depth into a depth function that computes thisk. As a first try, we may define

  1.  let rec depth = function
  2.     | List _ -> 1
  3.     | Nested n -> 1 + depth n;;
  4. Error: This expression has type 'a list nested
  5.        but an expression was expected of type 'a nested
  6.        The type variable 'a occurs inside 'a list

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 oneleads to the impossible constraint 'a list nested = 'a nested.In other words, within its definition, the recursive function depth isapplied to values of type 'a t with different types 'a due to thenon-regularity of the type constructor nested. This creates a problem becausethe type checker had introduced a new type variable 'a only at thedefinition of the function depth whereas, here, we need adifferent type variable for every application of the function depth.

5.2.1 Explicitly polymorphic annotations

The solution of this conundrum is to use an explicitly polymorphic typeannotation for the type 'a:

  1.  let rec depth: 'a. 'a nested -> int = function
  2.     | List _ -> 1
  3.     | Nested n -> 1 + depth n;;
  4. val depth : 'a nested -> int = <fun>
  1.  depth ( Nested(List [ [7]; [8] ]) );;
  2. - : int = 2

In the type of depth, 'a.'a nested -> int, the type variable 'ais 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 interpretedas “let be a type variable 'a, then depth maps 'a nested valuesto integers”. There are two major differences with these two typeexpressions. First, the explicit polymorphic annotation indicates to thetype checker that it needs to introduce a new type variable every timesthe function depth is applied. This solves our problem with the definitionof the function depth.

Second, it also notifies the type checker that the type of the function shouldbe polymorphic. Indeed, without explicit polymorphic type annotation, thefollowing type annotation is perfectly valid

  1.    let sum: 'a -> 'b -> 'c = fun x y -> x + y;;
  2. val sum : int -> int -> int = <fun>

since 'a,'b and 'c denote type variables that may or may not bepolymorphic. Whereas, it is an error to unify an explicitly polymorphic typewith a non-polymorphic type:

  1.    let sum: 'a 'b 'c. 'a -> 'b -> 'c = fun x y -> x + y;;
  2. Error: This definition has type int -> int -> int which is less general than
  3.          'a 'b 'c. 'a -> 'b -> 'c

An important remark here is that it is not needed to explicit fullythe type of depth: it is sufficient to add annotations only for theuniversally quantified type variables:

  1.  let rec depth: 'a. 'a nested -> _ = function
  2.     | List _ -> 1
  3.     | Nested n -> 1 + depth n;;
  4. val depth : 'a nested -> int = <fun>
  1.  depth ( Nested(List [ [7]; [8] ]) );;
  2. - : int = 2

5.2.2 More examples

With explicit polymorphic annotations, it becomes possible to implementany recursive function that depends only on the structure of the nestedlists and not on the type of the elements. For instance, a more complexexample would be to compute the total number of elements of the nestedlists:

  1.    let len nested =
  2.       let map_and_sum f = List.fold_left (fun acc x -> acc + f x) 0 in
  3.       let rec len: 'a. ('a list -> int ) -> 'a nested -> int =
  4.       fun nested_len n ->
  5.         match n with
  6.         | List l -> nested_len l
  7.         | Nested n -> len (map_and_sum nested_len) n
  8.       in
  9.     len List.length nested;;
  10. val len : 'a nested -> int = <fun>
  1.  len (Nested(Nested(List [ [ [1;2]; [3] ]; [ []; [4]; [5;6;7]]; [[]] ])));;
  2. - : int = 7

Similarly, it may be necessary to use more than one explicitlypolymorphic type variables, like for computing the nested list oflist lengths of the nested list:

  1.  let shape n =
  2.     let rec shape: 'a 'b. ('a nested -> int nested) ->
  3.       ('b list list -> 'a list) -> 'b nested -> int nested
  4.       = fun nest nested_shape ->
  5.         function
  6.         | List l -> raise
  7.          (Invalid_argument "shape requires nested_list of depth greater than 1")
  8.         | Nested (List l) -> nest @@ List (nested_shape l)
  9.         | Nested n ->
  10.           let nested_shape = List.map nested_shape in
  11.           let nest x = nest (Nested x) in
  12.           shape nest nested_shape n in
  13.     shape (fun n -> n ) (fun l -> List.map List.length l ) n;;
  14. val shape : 'a nested -> int nested = <fun>
  1.  shape (Nested(Nested(List [ [ [1;2]; [3] ]; [ []; [4]; [5;6;7]]; [[]] ])));;
  2. - : int nested = Nested (List [[2; 1]; [0; 1; 3]; [0]])

5.3 Higher-rank polymorphic functions

Explicit polymorphic annotations are however not sufficient to cover allthe cases where the inferred type of a function is less general thanexpected. A similar problem arises when using polymorphic functions as argumentsof higher-order functions. For instance, we may want to compute the averagedepth or length of two nested lists:

  1.    let average_depth x y = (depth x + depth y) / 2;;
  2. val average_depth : 'a nested -> 'b nested -> int = <fun>
  1.    let average_len x y = (len x + len y) / 2;;
  2. val average_len : 'a nested -> 'b nested -> int = <fun>
  1.    let one = average_len (List [2]) (List [[]]);;
  2. val one : int = 1

It would be natural to factorize these two definitions as:

  1.      let average f x y = (f x + f y) / 2;;
  2. val average : ('a -> int) -> 'a -> 'a -> int = <fun>

However, the type of average len is less generic than the type ofaverage_len, since it requires the type of the first and second argument tobe the same:

  1.    average_len (List [2]) (List [[]]);;
  2. - : int = 1
  1.    average len (List [2]) (List [[]]);;
  2. Error: This expression has type 'a list
  3.        but an expression was expected of type int

As previously with polymorphic recursion, the problem stems from the fact thattype variables are introduced only at the start of the let definitions. Whenwe 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 checkerthat f is polymorphic in its first argument. In some sense, we would wantaverage to have type

  1. val average: ('a. 'a nested -> int) -> 'a nested -> 'b nested -> int

Note that this syntax is not valid within OCaml: average has an universallyquantified type 'a inside the type of one of its argument whereas forpolymorphic recursion the universally quantified type was introduced beforethe rest of the type. This position of the universally quantified type meansthat average is a second-rank polymorphic function. This kind of higher-rankfunctions is not directly supported by OCaml: type inference for second-rankpolymorphic function and beyond is undecidable; therefore using this kind ofhigher-rank functions requires to handle manually these universally quantifiedtypes.

In OCaml, there are two ways to introduce this kind of explicit universallyquantified types: universally quantified record fields,

  1.    type 'a nested_reduction = { f:'elt. 'elt nested -> 'a };;
  2. type 'a nested_reduction = { f : 'elt. 'elt nested -> 'a; }
  1.    let boxed_len = { f = len };;
  2. val boxed_len : int nested_reduction = {f = <fun>}

and universally quantified object methods:

  1.    let obj_len = object method f:'a. 'a nested -> 'b = len end;;
  2. val obj_len : < f : 'a. 'a nested -> int > = <obj>

To solve our problem, we can therefore use either the record solution:

  1.    let average nsm x y = (nsm.f x + nsm.f y) / 2 ;;
  2. val average : int nested_reduction -> 'a nested -> 'b nested -> int = <fun>

or the object one:

  1.    let average (obj:<f:'a. 'a nested -> _ > ) x y = (obj#f x + obj#f y) / 2 ;;
  2. val average : < f : 'a. 'a nested -> int > -> 'b nested -> 'c nested -> int =
  3.   <fun>