[Caml-list] Re: References and polymorphism

[Dawid Toton <d0@wp.pl>]

On 2012-01-11 14:15, rossberg@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