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