polymorphic type vs weak type

user_4489902 0
Viewed 88

I try to write a reverse function for a polymorphic list as shown.

let rev  =
  let rec impl_rec acc = function
    | []    -> acc
    | x::xs -> impl_rec (x::acc) xs 
  in impl_rec []

The compiler infers a type of

'_weak list -> '_weak list

However, If I provide the parameter explicitly.

let rev xs  =
  let rec impl_rec acc = function
    | []    -> acc
    | x::xs -> impl_rec (x::acc) xs 
  in impl_rec [] xs

The following code is able to infer the polymorphic type

'a list -> 'a list

There is no ref type. How does the OCaml Compiler infer the first version to a weak type?

ocaml functional-programming
1 Answers

This is the value restriction at work: https://ocaml.org/manual/polymorphism.html#s:weak-polymorphism . The value restriction makes a difference between values, for instance

fun x -> x,
Constructor value,
(value, value')

and computation

f x
{ contents = [] } (* contents is a mutable field *)

Outside of the relaxed value restriction (which applies mostly to empty containers), only syntactic values may be polymorphic and any computation is given a weakly polymorphic type. Typically, in your first implementation:

let rev =
   ...
   impl_rec []

the function rev is the result of a computation and thus cannot be made polymorphic. Contrarily, in

let rev = fun l -> ... impl_rec [] l

the function rev is syntactically a function and thus a syntactic value. Its type can therefore be generalized.

The pragmatic summary is that if you are building a function for later uses in OCaml, it is better to ensure that it is also a syntactic function to avoid the value restriction.

On a higher-level, this illustrates the fact that the value restriction is an approximation. It allows mutable values and polymorphism to coexist without unsoundness and without having to refine the type of functions into several different arrow types. But this come at the cost of some overly cautious introduction of weakly polymorphic type.

user_73693660
Related