On 2012-01-11 12:43, [email protected] wrote:
Dawid Toton wrote:
Why not to just forbid too general 'a ref types? See the example from
the page cited above (with explicit quantifier added):
let f : forall 'a. 'a -> 'a =
let r : 'a option ref = ref None in
fun x -> (* do evil things with the ref cell *)
let y = !r in
let () = r := Some x in
match y with
| None -> x
| Some y -> y
The problem is that the 'a variable is bound by a general quantifier and
at the same time it is used to give a type to the ref cell. But if this
were forbidden, I see no need for the value restriction at all. For example:
let g : forall 'a. 'a -> 'a =
fun (x : exists 'b. 'b) ->
let r : 'b option ref = ref None in
(* nothing bad can happen *)
...
Nothing useful can happen either. You could never read a value back from r
and use/return it as an 'a or for anything else. So why would you want to
store it there in the first place?
I can read from r and use it as 'b option. This is useful in general: a
mutable store can be used locally to speed up computations. I can
imagine working on 'b array to benefit from fast lookup.
Also, I don't quite understand how your type annotations are supposed to
match up. If x : exists 'b. 'b, then f can't be forall 'a. 'a -> 'a.
Use de Morgan's laws for quantifiers:
(∃x. x) → y
¬((∃x. x) ∧ ¬y)
¬(∃x. (x ∧ ¬y))
∀x.(¬(x ∧ ¬y))
∀x.(x → y)
I see, this is probably abuse of constructive logic in this case, but I
believe the idea stays the same.
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
