Re: [Caml-list] Re: References and polymorphism

[rossberg@mpi-sws.org]

Dawid Toton wrote:
> 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.

It is actually:

d) computation is not suspended, allocation is done when the declaration is
evaluated, for some.

That is more or less equivalent to (c) when the declaration is in global scope.

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

/Andreas