Re: [Caml-list] Why doesn't relaxed value restriction apply here?

[Jeremy Yallop <yallop@gmail.com>]

On 21 April 2018 at 10:14, Romain Bardou <romain@bardou.fr> wrote:
> On 04/21/2018 11:04 AM, Jeremy Yallop wrote:
>>
>> On 21 April 2018 at 09:41, Romain Bardou <romain@bardou.fr> wrote:
>>>
>>> According to the manual
>>> (http://caml.inria.fr/pub/docs/manual-ocaml/polymorphism.html) and to the
>>> paper "Relaxing the Value Restriction"
>>>
>>> (http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf),
>>> the relaxed value restriction allows to generalize type variables which
>>> only
>>> appear in covariant positions.
>>>
>>> The following code :
>>>
>>>      let f = let _ = ref 0 in fun f -> f []
>>>
>>> returns the following in the toplevel:
>>>
>>>      val f : ('_a list -> '_b) -> '_b = <fun>
>>>
>>> In this type, '_a only appears in covariant position. So, why is it not
>>> generalized?
>>
>>
>> I think the current implementation only generalizes variables that
>> only occur in *strictly* positive positions -- that is, that do not
>> appear to the left of any arrow.  In your example, "'a" occurs in a
>> positive position (to the left of an even number of arrows) that is
>> not strictly positive (to the left of zero arrows).
>
>
> Interesting. I wonder what the reason is behind this choice: is it about
> soundness, or about simplicity. Your example below seems to indicate that
> this is not about soundness as one can hide the depth of a type variable
> using an abstract type.

I think it's about principality.  Since type variables in
contravariant positions are not generalized, the following definition
of 'h' receives a non-polymorphic type:

   let h = (fun x -> x) (fun _ -> ())
   val h : '_a -> unit

and so a program that uses 'h' with some arbitrary argument type is allowed

   let m = h ()

but a program that use 'h' at multiple types is rejected:

   let p = (h print_int, h print_float)

However, 'h' could also be given the less general type ('b -> unit) ->
unit, in which the type variable only appears in covariant positions.
If this type variable were generalized then 'p' would be allowed, but
'm' would be rejected: there's no longer a best type for 'h' that can
be determined solely from its definition.  The restriction to strictly
positive positions avoids this situation.

>> This choice can lead to some slightly surprising situations, where
>> exposing valid type equalities can cause previously-valid programs to
>> be rejected.  For example, the following program, which is based on
>> your example, is accepted:
>>
>>     module M :
>>     sig
>>       type (+'a,'b) t
>>       val g : unit -> ('a,'b) t
>>     end =
>>     struct
>>       type (+'a,'b) t = ('a list -> 'b) -> 'b
>>       let g () = let _ = ref 0 in fun f -> f []
>>     end;;
>>
>>     let f = M.g () in ((f : (int, unit) M.t), (f : (float, unit) M.t));;
>>
>> but if the signature for 'M' is removed then the program is rejected.
>
> That's very interesting actually.

There are a few such ways to break OCaml programs by exposing type
equalities: something similar happens with unboxed float records, and
with GADT exhaustiveness checking. (Details left as an exercise for
the reader!)