[Caml-list] The value restriction

[Caml-list] The value restriction

[Andrej Bauer]

Can someone explain this behavior?

# ([], (fun x -> x) (fun y -> y)) ;;
- : 'a list * ('_b -> '_b) = ([], <fun>)

# ((fun a -> a), (fun x -> x) (fun y -> y)) ;;
- : ('_a -> '_a) * ('_b -> '_b) = (<fun>, <fun>)

Why does the second component influence the first one (in a non-obvious way)?

With kind regards,

Andrej

Re: [Caml-list] The value restriction

[Gabriel Scherer]

[-- Attachment #1: Type: text/plain, Size: 1834 bytes --]

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.


On Fri, Dec 16, 2011 at 10:18 AM, Andrej Bauer <andrej.bauer@andrej.com>wrote:

> Can someone explain this behavior?
>
> # ([], (fun x -> x) (fun y -> y)) ;;
> - : 'a list * ('_b -> '_b) = ([], <fun>)
>
> # ((fun a -> a), (fun x -> x) (fun y -> y)) ;;
> - : ('_a -> '_a) * ('_b -> '_b) = (<fun>, <fun>)
>
> Why does the second component influence the first one (in a non-obvious
> way)?
>
> With kind regards,
>
> Andrej
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

[-- Attachment #2: Type: text/html, Size: 2736 bytes --]

Re: [Caml-list] The value restriction

[Didier Remy]

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