Re: [Caml-list] The value restriction

[Gabriel Scherer <gabriel.scherer@gmail.com>]

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