Re: [Caml-list] The value restriction

[Didier Remy <Didier.Remy@inria.fr>]

On 12/16/2011 10:39 AM, Gabriel Scherer wrote:
> The following example, derived from yours, is probably more surprised (I didn't
> understand your issue at first):
>
>    # ((fun a -> a), (fun b -> b));;
>    - : ('a -> 'a) * ('b -> 'b) = (<fun>, <fun>)
>    # ((fun a -> a), (fun b -> b) (fun c -> c));;
>    - : ('_a -> '_a) * ('_b -> '_b) = (<fun>, <fun>)
>
> Here is how I explain this from the paper "Relaxing the value restriction",
> Jacques Garrigue, 2004:
> http://caml.inria.fr/about/papers.en.html
> No guarantee that this matches the actual typing behavior.
>
> There are two different typing rules: one for the form "let x = v in e", where a
> value is bound, all typing variables are generalized, and one other for the form
> "let x = e1 in e2", where an *expression* is bound, and all non-negative
> variables are generalized.
>
> In the ((fun a -> a), (fun b -> b)) example, this is a value, everything gets
> generalized. In the ((fun a -> a), (fun b -> b) (fun c -> c)) example, this is
> not a value anymore, and both components use a type variable in negative
> position, so nothing gets generalized. In the ([], (fun b -> b) (fun c -> c))
> example, this is not a value but [] is covariant in its type variable, so it
> still gets generalized.

Yes, this is the reason.

The only influence of the second component is that the pair itself is not a
value, in both cases.  The differences you observed is only due to the
differences in the (types of the) first component.

Perhaps, you expected that the type of first component of the pair could be
generalized in both cases because it is a value.

There is a known improvement of the value restriction that would allow this
generalization: the rule would say "type variables appearing in the type of
*expansive* expressions cannot be generalized".  Intuitively, expansive
expressions are expressions whose evaluation could allocate a piece of
mutable store.  In the example above the pair itself is non expansive (it is
a constructor), the first component is not expansive (it is a value); only
the second component is expansive (it is an application).  Hence, only type
variables appearing in the second component cannot be generalized.

However, this improvement is not implemented in OCaml.

         Didier