On 2012-01-11 14:15, rossb...@mpi-sws.org 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.
I would insist that it won't crash at run-time.
Consider the possibilities:
a) type abstraction suspends the computation - no run-time crash; there
are implementation problems as in my comment above
b) computation is not suspended in the sense that the job is done at
compile time - for each possible type 'aa a separate ref cell is
allocated. This is of course problematic in practice, but still sound.
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.
I would say that the difference between a) and b) is minor, just a
choice between more static or more dynamic implementation of the same
semantics.
The c) option is incorrect, as I understand it, regardless what type
system flavour is chosen.
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
