Value restriction for records

Question

I face a situation where a record is given a weak polymorphic type and I am not sure why.

Here is a minimized example

module type S = sig
  type 'a t
  val default : 'a t
end

module F (M : S) = struct
  type 'a record = { x : 'a M.t; n : int }

  let f = { x = M.default; n = (fun x -> x) 3 }
end

Here f is given the type '_weak1 record.

There are (at least) two ways to solve that problem.

• The first one consists in using an auxiliary definition for the function application.

  let n = (fun x -> x) 3
  let f = { x = M.default; n }
  

• The second one consists in declaring the type parameter of t as covariant.

  module type S = sig
     type +'a t
     val default : 'a t
  end
  

What I find strange is that the function application is used to initialize the field of type int that has no link at all with the type variable 'a of type t. And I also fail to see why declaring 'a as covariant suddenly allows to use arbitrary expressions in this unrelated field without losing polymorphism.

Acrylonitrile

Answer 1

For your first point, the relaxed value restriction is triggered as soon as any computation happens in any sub-expression. Thus neither

{ x = M.default; n = (fun x -> x) 3 }

nor

let n = Fun.id 3 in { x = M.default; n }

are considered a value and the value expression applies to both of them.

For your second point, this the relaxed value restriction at work: if a type variable only appears in strictly covariant positions, it can always be generalized. For instance, the type of

let none = Fun.id None

is 'a. 'a option and not '_weak1 option because the option type constructor is covariant in its first parameter.

The brief explanation for this relaxation of the value restriction is that a covariant type parameter corresponds to a positive immutable piece of data, for instance

type !+'a option = None | Some of 'a

or

type +'a t = A

Thus if we have a type variable that only appear in strictly covariant position, we know that it is not bound to any mutable data, and it can thus be safely generalized.

An important point to notice however, if that the only values of type 'a t for a t covariant in its first parameters are precisely those that does not contains any 'a. Thus, if I have a value of type 'a. 'a option, I know that I have in fact a None. We can in fact check that point with the help of the typechecker:

type forall_option = { x:'a. 'a option }
type void = |
let for_all_option_is_none {x} = match (x: void option) with
| None -> ()
| _ -> . (* this `.` means that this branch cannot happen *)

Here by constraining the type 'a. 'a option to void option, we have made the typechecker aware than x was in fact a None.

Tocantins

Thanks for the intuition that, if a type is covariant in its type parameter, terms of polymorphic type basically store no data of the underlying type! The OCaml excerpt is really convincing too! – Acrylonitrile

What puzzles me is that I don't see how a term of the kind I gave in my question can be harmful if it is given a polymorphic type. Is it just that the (relaxed) value restriction is too conservative in this case? Or is it possible to forge a nasty term of the same shape that would be problematic if being defined with a polymorphic type? – Acrylonitrile

The value restriction is too restrictive here because it does not analyze separately the two sides of the product: here the computation and the polymorphic type happens in a separate side of the product, but the whole product is deemed as a non-value and restricted to non-polymorphic types. – Tocantins