On 2012-01-11 16:42, [email protected] wrote:
Dawid Toton wrote:
On 2012-01-11 14:15, [email protected] wrote:
let f3 : forall ÂÂ'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). *)
No, this would be unsound, because "fun (type t) -> ..." does not the
suspend computation -- there'd be only one ref. It's not System F.
c) computation is not suspended in the sense that the allocation is done
at compile time, but the implementation tries to keep only one ref cell
for this purpose. This is impossible. The function can't be compiled
this way.
It is actually:
d) computation is not suspended, allocation is done when the declaration is
evaluated, for some.
The c) option is incorrect, as I understand it, regardless what type
system flavour is chosen.
Not sure why you think so, but in any case, that's essentially what's
happening. Type abstraction or application is not operationally observable
in OCaml, or any similar language. Which is exactly the reason why the
whole soundness issue with polymorphism + references arises, and you have to
disallow certain combinations.
This specific example, the f3 function, won't happen in OCaml-like
language at all, because of the forall quantifier in type annotation for
the function. While I get the point that this generalization is
forbidden by the value restriction, what I'm trying to say is that the
value restriction is not needed here and I can't think of any convincing
example in favour of if.
Here is how we get the right result without the value restriction rule:
first the compiler has to choose the strategy (a), (b) or (c/d). For (a)
and (b) it can say that it isn't smart enough and refuse to compile the
code. On the other hand, the (c/d) case is rejected, because of the
impossible allocation of r: types int list ref and string list ref are
incompatible, hence one allocation for all the cases is insufficient.
This is so simple, because we are not interested in generalized ref
cells, I mean, values of forall 'a.('a list ref) types are useless and I
think that less sophisticated typechecker shouldn't even consider this type.
It is perhaps more clear if said this way: the strategy (c/d) is
equivalent to starting with the f0/f2 function body in order to build
something equivalent to f3. But f2 cannot be cast to f3, because (r :
∀'c. 'c list) allocated in f2 cannot be cast to 'aa list ref. An error
message would say that types 'c and 'aa cannot be unified, or - if the
quantifier for the function type is yet to be chosen - typechecker would
give up with forall and continue with a type variable (a type exists).
In case of ordinary OCaml, things are even simpler. One can't express
f3. My current understanding is that only f4 and the following are possible:
∃'b.
let f : X 'a. (unit -> 'a list ref) =
let r = ref ([] : 'b list) in
fun (type 'aa) ->
fun () ->
r
Only existential quantifier will fit X so the whole thing is well typed.
Again, no value restriction intervenes.
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
