[Caml-list] Re: References and polymorphism

[Dawid Toton <d0@wp.pl>]

On 2012-01-11 12:07, Gabriel Scherer wrote:
> How would you make the distinction between
>
>    let f : 'a . unit ->  'a list ref =
>      fun () ->  ref ([] : 'a list)
>
> and
>
>    let f : 'a . unit ->  'a list ref =
>      let r = ref ([] : 'a list) in
>      fun () ->  r
>
> ?
>
I think that it's not the value restriction which prevents the second 
example from have generalized type.
Here's how I uderstand it.

First, we write the code, but don't put a quantifier in the annotation 
for f:

let f : unit ->  'a list ref =
   let r = ref ([] : 'a list) in
   fun () ->  r


Then, compiler tries to determine what does it mean. I think it should 
see it in the following way:

∃'b.
let f : X 'a. (unit -> 'a list ref) =
   let r = ref ([] : 'b list) in
   fun () -> r

where X stays for an unknown quantifier: generalize or not? We can try 
with forall:

∃'b.
let f : ∀ 'a. (unit -> 'a list ref) =
   let r = ref ([] : 'b list) in
   fun () -> r

But this doesn't typecheck: you cannot pass a value of type 'b list ref 
with some particular 'b and pretend that it works for some unrelated 'a.

A second possibility:
∃'b.
let f : ∃'a. (unit -> 'a list ref) =
   let r = ref ([] : 'b list) in
   fun () -> r

Here, nothing special happens. The compiler discovers that 'a='b. The 
toplevel translates this quantification to an underscore and we get unit 
-> '_a list ref.

I have considered several variations around this theme and no one needs 
the extra value restriction rule:

∀'a.(
let f : unit -> 'a list ref =
   let r = ref ([] : 'a list) in
   fun () -> r
)

(* above: Anonymous mapping from types to functions. Useless. *)

let f0 : ∀'a. (unit -> ∀'b. 'b list ref) =
   let r = ref ([] : ∀'c. 'c list) in
   fun (type 'aa) ->
     fun () ->
       r

(* f0: Sound, but returns useless ref [] constant. Its type ∀'b. 'b list 
ref could be forbidden. *)

let f1 : ∀'a . (unit -> 'a list ref) =
   let r = ref ([] : 'a list) in
   fun (type 'aa) ->
     fun () ->
       r

(* f1: Problem with type variable scope. The quantifier encompasses what 
is in brackets in the annotation for f1. Function body cannot refer to 
'a bound by this quantifier. It wouldn't make sense. *)

let f2 : ∀'a . (unit -> 'a list ref) =
   let r = ref ([] : ∀'c. 'c list) in
   fun (type 'aa) ->
     fun () ->
       r

(* f2: Type of function body (for each type return a constant/degenerate 
cell) is incompatible with the type given in the annotation (for each 
type return an useful ref cell). But it would be simpler just to avoid 
the useless type of r entirely. *)

let f3 : ∀'a . unit -> 'a list ref =
   fun (type 'aa) ->
     let r = ref ([] : 'aa list) in
     fun () ->
       r

(* f3: Fine, but it would require some work at compile time or smart 
transformations to keep types erased at run-time. Also, keeping the 
first actual argument (staying for 'aa) implicit would need extra rules 
to resolve ambiguities (decide when this argument is applied). *)

let f4 : ∀'a . unit -> 'a list ref =
   fun (type 'aa) ->
     fun () ->
       let r = ref ([] : 'aa list) in
       r

(* f4: All clear. *)

Dawid