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

[Romain Bardou <romain@bardou.fr>]

On 04/21/2018 11:45 AM, Jeremy Yallop wrote:
> 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.

I see, it makes sense.

>>> 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!)

Now that you mention it, I already encountered this issue several times 
with GADTs. It was rather annoying actually.

Thanks again, this really helped

Cheers,

-- 
Romain Bardou

-- 
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs