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

[Dawid Toton <d0@wp.pl>]

On 2012-01-11 16:42, rossberg@mpi-sws.org wrote:
> 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.
>> 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