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

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

[Romain Bardou]

Hello,

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?

Sorry if this has been asked already, I could not find anything. I'm 
sure there is a simple explanation. I can't find out whether:
- I'm stupid and '_a actually appears in a non-covariant position;
- I'm stupid and read the rule about relaxed value restriction wrong;
- or the relaxed value restriction which was implemented is not actually 
the one which is described in the manual and in the paper.

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

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

[Jeremy Yallop]

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

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.

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

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

[Romain Bardou]

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.

> 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.

Thanks a lot for your quick answer and your example :)

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

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

[Jeremy Yallop]

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

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

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

[Romain Bardou]

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