[Caml-list] References and polymorphism

[Caml-list] References and polymorphism

[Dario Teixeira]

Hi,

Consider functions foobar1 and foobar2:


type 'a t = {id: int; x: 'a}

let foobar1: 'a -> 'a t =
        fun x -> {id = 0; x}

let foobar2: 'a -> 'a t =
        let ctr = ref 0 in
        fun x -> incr ctr; {id = !ctr; x}



I would expect them to have the same type, because foobar2's
use of a reference cell is kept private.  However, they don't.
In fact, foobar2 is not really polymorphic:


type 'a t = { id : int; x : 'a; }
val foobar1 : 'a -> 'a t
val foobar2 : '_a -> '_a t


It's easy to get around this issue by putting the reference cell
outside of foobar2.  Function foobar3 does just this, and behaves
as expected:


let next =
        let ctr = ref 0 in
        fun () -> incr ctr; !ctr

let foobar3: 'a -> 'a t =
        fun x -> {id = next (); x}



Could someone point me to a good explanation of what's going on?
(I have the feeling I've read about this restriction before.)

Best regards,
Dario Teixeira

Re: [Caml-list] References and polymorphism

[Romain Bardou]

Le 10/01/2012 16:29, Dario Teixeira a écrit :
> Hi,
>
> Consider functions foobar1 and foobar2:
>
>
> type 'a t = {id: int; x: 'a}
>
> let foobar1: 'a ->  'a t =
>          fun x ->  {id = 0; x}
>
> let foobar2: 'a ->  'a t =
>          let ctr = ref 0 in
>          fun x ->  incr ctr; {id = !ctr; x}
>
>
>
> I would expect them to have the same type, because foobar2's
> use of a reference cell is kept private.  However, they don't.
> In fact, foobar2 is not really polymorphic:
>
>
> type 'a t = { id : int; x : 'a; }
> val foobar1 : 'a ->  'a t
> val foobar2 : '_a ->  '_a t
>
>
> It's easy to get around this issue by putting the reference cell
> outside of foobar2.  Function foobar3 does just this, and behaves
> as expected:
>
>
> let next =
>          let ctr = ref 0 in
>          fun () ->  incr ctr; !ctr
>
> let foobar3: 'a ->  'a t =
>          fun x ->  {id = next (); x}
>
>
>
> Could someone point me to a good explanation of what's going on?
> (I have the feeling I've read about this restriction before.)
>
> Best regards,
> Dario Teixeira
>
>
>

Hello,

This is, basically, the value restriction: you cannot let-generalize 
something which is not *syntactically* a value. Function foobar1 is 
syntactically a function, and a function is a value. Function foobar2 is 
not: it starts with a let-binding. It computes something before 
returning a function. It cannot be generalized.

Cheers,

-- 
Romain Bardou

Re: [Caml-list] References and polymorphism

[Arnaud Spiwack]

[-- Attachment #1: Type: text/plain, Size: 2399 bytes --]

I guess a canonical example of the reason behind this restriction would be
the following:

let put = let r = ref [] in fun x -> r := x::!r

OCaml will tell you that it has type '_a -> unit. It would be unsound
(exercise!) to decide it has type 'a -> unit.

Of course, your example is perfectly sound, but the typing algorithm
doesn't know that.

--
Arnaud Spiwack

On 10 January 2012 16:45, Romain Bardou <bardou@lsv.ens-cachan.fr> wrote:

> Le 10/01/2012 16:29, Dario Teixeira a écrit :
>
>  Hi,
>>
>> Consider functions foobar1 and foobar2:
>>
>>
>> type 'a t = {id: int; x: 'a}
>>
>> let foobar1: 'a ->  'a t =
>>         fun x ->  {id = 0; x}
>>
>> let foobar2: 'a ->  'a t =
>>         let ctr = ref 0 in
>>         fun x ->  incr ctr; {id = !ctr; x}
>>
>>
>>
>> I would expect them to have the same type, because foobar2's
>> use of a reference cell is kept private.  However, they don't.
>> In fact, foobar2 is not really polymorphic:
>>
>>
>> type 'a t = { id : int; x : 'a; }
>> val foobar1 : 'a ->  'a t
>> val foobar2 : '_a ->  '_a t
>>
>>
>> It's easy to get around this issue by putting the reference cell
>> outside of foobar2.  Function foobar3 does just this, and behaves
>> as expected:
>>
>>
>> let next =
>>         let ctr = ref 0 in
>>         fun () ->  incr ctr; !ctr
>>
>> let foobar3: 'a ->  'a t =
>>         fun x ->  {id = next (); x}
>>
>>
>>
>> Could someone point me to a good explanation of what's going on?
>> (I have the feeling I've read about this restriction before.)
>>
>> Best regards,
>> Dario Teixeira
>>
>>
>>
>>
> Hello,
>
> This is, basically, the value restriction: you cannot let-generalize
> something which is not *syntactically* a value. Function foobar1 is
> syntactically a function, and a function is a value. Function foobar2 is
> not: it starts with a let-binding. It computes something before returning a
> function. It cannot be generalized.
>
> Cheers,
>
> --
> Romain Bardou
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/**wws/info/caml-list<https://sympa-roc.inria.fr/wws/info/caml-list>
> Beginner's list: http://groups.yahoo.com/group/**ocaml_beginners<http://groups.yahoo.com/group/ocaml_beginners>
> Bug reports: http://caml.inria.fr/bin/caml-**bugs<http://caml.inria.fr/bin/caml-bugs>
>
>

[-- Attachment #2: Type: text/html, Size: 3276 bytes --]

Re: [Caml-list] References and polymorphism

[Dario Teixeira]

Hi,

Thank you, Romain and Arnaud.  With that "list ref" example in mind,
it does make sense for the compiler to play it safe and declare foobar2
to be non-polymorphic.  Moreover, this is one of those issues where I
I suspect that compiler elfs must have pondered already how easy/feasible
it would be to extend the compiler to detect sound instances (such as foobar2)
that could be accepted...

Cheers,
Dario Teixeira

RE: [Caml-list] References and polymorphism

[David Allsopp]

Dario Teixeira wrote:
> Thank you, Romain and Arnaud.  With that "list ref" example in mind, it
> does make sense for the compiler to play it safe and declare foobar2 to
> be non-polymorphic.  Moreover, this is one of those issues where I I
> suspect that compiler elfs must have pondered already how easy/feasible
> it would be to extend the compiler to detect sound instances (such as
> foobar2) that could be accepted...

They certainly did: http://mlton.org/ValueRestriction has links to the various papers on the subject (the present scheme was not the first solution for SML, as it notes). 


David

Re: [Caml-list] References and polymorphism

[Gabriel Scherer]

For a description of how the value restriction is relaxed in the OCaml
type system, see the article
  "Relaxing the value restriction", by Jacques Garrigue, 2004
  http://caml.inria.fr/about/papers.en.html

On Tue, Jan 10, 2012 at 6:20 PM, David Allsopp <dra-news@metastack.com> wrote:
> Dario Teixeira wrote:
>> Thank you, Romain and Arnaud.  With that "list ref" example in mind, it
>> does make sense for the compiler to play it safe and declare foobar2 to
>> be non-polymorphic.  Moreover, this is one of those issues where I I
>> suspect that compiler elfs must have pondered already how easy/feasible
>> it would be to extend the compiler to detect sound instances (such as
>> foobar2) that could be accepted...
>
> They certainly did: http://mlton.org/ValueRestriction has links to the various papers on the subject (the present scheme was not the first solution for SML, as it notes).
>
>
> David
>
>
> --
> 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
>

[Caml-list] Re: References and polymorphism

[Dawid Toton]

> They certainly did: http://mlton.org/ValueRestriction has links to the various papers on the subject (the present scheme was not the first solution for SML, as it notes).
>
I don't get one thing about this. It seems that all examples which 
justify the value restriction are unsound just because a ref cell is 
given too general type.
Why not to just forbid too general 'a ref types? See the example from 
the page cited above (with explicit quantifier added):

let f : forall 'a. 'a -> 'a =
   let r : 'a option ref = ref None in
   fun x -> (* do evil things with the ref cell *)
     let y = !r in
     let () = r := Some x in
     match y with
       | None -> x
       | Some y -> y

The problem is that the 'a variable is bound by a general quantifier and 
at the same time it is used to give a type to the ref cell. But if this 
were forbidden, I see no need for the value restriction at all. For example:

let g : forall 'a. 'a -> 'a =
   fun (x : exists 'b. 'b) ->
     let r : 'b option ref = ref None in
     (* nothing bad can happen *)
     ...

Dawid

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

[Gabriel Scherer]

How would you make the distinction between

  let f : 'a . unit -> 'a list ref =
    fun () -> ref ([] : 'a list)

and

  let f : 'a . unit -> 'a list ref =
    let r = ref ([] : 'a list) in
    fun () -> r

?

On Wed, Jan 11, 2012 at 11:48 AM, Dawid Toton <d0@wp.pl> wrote:
>> They certainly did: http://mlton.org/ValueRestriction has links to the
>> various papers on the subject (the present scheme was not the first solution
>> for SML, as it notes).
>>
> I don't get one thing about this. It seems that all examples which justify
> the value restriction are unsound just because a ref cell is given too
> general type.
> Why not to just forbid too general 'a ref types? See the example from the
> page cited above (with explicit quantifier added):
>
> let f : forall 'a. 'a -> 'a =
>  let r : 'a option ref = ref None in
>  fun x -> (* do evil things with the ref cell *)
>    let y = !r in
>    let () = r := Some x in
>    match y with
>      | None -> x
>      | Some y -> y
>
> The problem is that the 'a variable is bound by a general quantifier and at
> the same time it is used to give a type to the ref cell. But if this were
> forbidden, I see no need for the value restriction at all. For example:
>
> let g : forall 'a. 'a -> 'a =
>  fun (x : exists 'b. 'b) ->
>    let r : 'b option ref = ref None in
>    (* nothing bad can happen *)
>    ...
>
> 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
>

[Caml-list] Re: References and polymorphism

[Dawid Toton]

On 2012-01-11 12:07, Gabriel Scherer wrote:
> How would you make the distinction between
>
>    let f : 'a . unit ->  'a list ref =
>      fun () ->  ref ([] : 'a list)
>
> and
>
>    let f : 'a . unit ->  'a list ref =
>      let r = ref ([] : 'a list) in
>      fun () ->  r
>
> ?
>
I think that it's not the value restriction which prevents the second 
example from have generalized type.
Here's how I uderstand it.

First, we write the code, but don't put a quantifier in the annotation 
for f:

let f : unit ->  'a list ref =
   let r = ref ([] : 'a list) in
   fun () ->  r


Then, compiler tries to determine what does it mean. I think it should 
see it in the following way:

∃'b.
let f : X 'a. (unit -> 'a list ref) =
   let r = ref ([] : 'b list) in
   fun () -> r

where X stays for an unknown quantifier: generalize or not? We can try 
with forall:

∃'b.
let f : ∀ 'a. (unit -> 'a list ref) =
   let r = ref ([] : 'b list) in
   fun () -> r

But this doesn't typecheck: you cannot pass a value of type 'b list ref 
with some particular 'b and pretend that it works for some unrelated 'a.

A second possibility:
∃'b.
let f : ∃'a. (unit -> 'a list ref) =
   let r = ref ([] : 'b list) in
   fun () -> r

Here, nothing special happens. The compiler discovers that 'a='b. The 
toplevel translates this quantification to an underscore and we get unit 
-> '_a list ref.

I have considered several variations around this theme and no one needs 
the extra value restriction rule:

∀'a.(
let f : unit -> 'a list ref =
   let r = ref ([] : 'a list) in
   fun () -> r
)

(* above: Anonymous mapping from types to functions. Useless. *)

let f0 : ∀'a. (unit -> ∀'b. 'b list ref) =
   let r = ref ([] : ∀'c. 'c list) in
   fun (type 'aa) ->
     fun () ->
       r

(* f0: Sound, but returns useless ref [] constant. Its type ∀'b. 'b list 
ref could be forbidden. *)

let f1 : ∀'a . (unit -> 'a list ref) =
   let r = ref ([] : 'a list) in
   fun (type 'aa) ->
     fun () ->
       r

(* f1: Problem with type variable scope. The quantifier encompasses what 
is in brackets in the annotation for f1. Function body cannot refer to 
'a bound by this quantifier. It wouldn't make sense. *)

let f2 : ∀'a . (unit -> 'a list ref) =
   let r = ref ([] : ∀'c. 'c list) in
   fun (type 'aa) ->
     fun () ->
       r

(* f2: Type of function body (for each type return a constant/degenerate 
cell) is incompatible with the type given in the annotation (for each 
type return an useful ref cell). But it would be simpler just to avoid 
the useless type of r entirely. *)

let f3 : ∀'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). *)

let f4 : ∀'a . unit -> 'a list ref =
   fun (type 'aa) ->
     fun () ->
       let r = ref ([] : 'aa list) in
       r

(* f4: All clear. *)

Dawid

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

[rossberg]

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

/Andreas

[Caml-list] Re: References and polymorphism

[Dawid Toton]

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

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

[rossberg]

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

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

[Dawid Toton]

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

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

[Andrej Bauer]

I would just like to remind the participants of this discussion that
the value restriction historically originated as a _simplifaction_ of
fancier and more capable forms of parametric polymorphism. The older,
more capable kinds of ML polymorphism grew increasingly more complex,
until Andrew Wright actually looked at what sort of programs people
wrote and noticed that for the most part the fancy stuff was not
needed. Thus it was decided that the ML polymorphism be _simplified_.
This was a good decision, as it made types easier to understand and
easier to implement, at a miniscule cost.

That is, we know that value restriction can be "improved", but by
trying to do so you are just repeating the mistakes that were alerady
made in the 90's.

With kind regards,

Andrej

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

[Romain Bardou]

Le 12/01/2012 11:05, Andrej Bauer a écrit :
> I would just like to remind the participants of this discussion that
> the value restriction historically originated as a _simplifaction_ of
> fancier and more capable forms of parametric polymorphism. The older,
> more capable kinds of ML polymorphism grew increasingly more complex,
> until Andrew Wright actually looked at what sort of programs people
> wrote and noticed that for the most part the fancy stuff was not
> needed. Thus it was decided that the ML polymorphism be _simplified_.
> This was a good decision, as it made types easier to understand and
> easier to implement, at a miniscule cost.
>
> That is, we know that value restriction can be "improved", but by
> trying to do so you are just repeating the mistakes that were alerady
> made in the 90's.
>
> With kind regards,
>
> Andrej
>

Some even argue, using the same kind of arguments, that (local) let 
should not be generalized [1]. Here we are not talking about local 
values though.

[1] Dimitrios Vytiniotis, Simon Peyton Jones and Tom Schrijvers, Let 
Should Not Be Generalised

-- 
Romain Bardou

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

[rossberg]

Dawid Toton wrote:
> Why not to just forbid too general 'a ref types? See the example from
> the page cited above (with explicit quantifier added):
>
> let f : forall 'a. 'a -> 'a =
>    let r : 'a option ref = ref None in
>    fun x -> (* do evil things with the ref cell *)
>      let y = !r in
>      let () = r := Some x in
>      match y with
>        | None -> x
>        | Some y -> y
>
> The problem is that the 'a variable is bound by a general quantifier and
> at the same time it is used to give a type to the ref cell. But if this
> were forbidden, I see no need for the value restriction at all. For example:
>
> let g : forall 'a. 'a -> 'a =
>    fun (x : exists 'b. 'b) ->
>      let r : 'b option ref = ref None in
>      (* nothing bad can happen *)
>      ...

Nothing useful can happen either. You could never read a value back from r
and use/return it as an 'a or for anything else. So why would you want to
store it there in the first place?

Also, I don't quite understand how your type annotations are supposed to
match up. If x : exists 'b. 'b, then f can't be forall 'a. 'a -> 'a.

/Andreas

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

[Dawid Toton]

On 2012-01-11 12:43, rossberg@mpi-sws.org wrote:
> Dawid Toton wrote:
>> Why not to just forbid too general 'a ref types? See the example from
>> the page cited above (with explicit quantifier added):
>>
>> let f : forall 'a. 'a ->  'a =
>>     let r : 'a option ref = ref None in
>>     fun x ->  (* do evil things with the ref cell *)
>>       let y = !r in
>>       let () = r := Some x in
>>       match y with
>>         | None ->  x
>>         | Some y ->  y
>>
>> The problem is that the 'a variable is bound by a general quantifier and
>> at the same time it is used to give a type to the ref cell. But if this
>> were forbidden, I see no need for the value restriction at all. For example:
>>
>> let g : forall 'a. 'a ->  'a =
>>     fun (x : exists 'b. 'b) ->
>>       let r : 'b option ref = ref None in
>>       (* nothing bad can happen *)
>>       ...
> Nothing useful can happen either. You could never read a value back from r
> and use/return it as an 'a or for anything else. So why would you want to
> store it there in the first place?
I can read from r and use it as 'b option. This is useful in general: a 
mutable store can be used locally to speed up computations. I can 
imagine working on 'b array to benefit from fast lookup.
> Also, I don't quite understand how your type annotations are supposed to
> match up. If x : exists 'b. 'b, then f can't be forall 'a. 'a ->  'a.
Use de Morgan's laws for quantifiers:

(∃x. x) → y

¬((∃x. x) ∧ ¬y)

¬(∃x. (x ∧ ¬y))

∀x.(¬(x ∧ ¬y))

∀x.(x → y)

I see, this is probably abuse of constructive logic in this case, but I 
believe the idea stays the same.
Dawid

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

[rossberg]

Dawid Toton wrote:
>>> The problem is that the 'a variable is bound by a general quantifier and
>>> at the same time it is used to give a type to the ref cell. But if this
>>> were forbidden, I see no need for the value restriction at all. For
>>> example:
>>>
>>> let g : forall 'a. 'a ->  'a =
>>>     fun (x : exists 'b. 'b) ->
>>>       let r : 'b option ref = ref None in
>>>       (* nothing bad can happen *)
>>>       ...
>> Nothing useful can happen either. You could never read a value back from r
>> and use/return it as an 'a or for anything else. So why would you want to
>> store it there in the first place?
>
> I can read from r and use it as 'b option. This is useful in general: a
> mutable store can be used locally to speed up computations. I can
> imagine working on 'b array to benefit from fast lookup.

But what do you do with that store? You can retrieve values from it, but
neither can use them locally (because they-re fully abstract) nor return
them (because they are not typed 'a). So it's useless to store them.

>> Also, I don't quite understand how your type annotations are supposed to
>> match up. If x : exists 'b. 'b, then f can't be forall 'a. 'a ->  'a.
> Use de Morgan's laws for quantifiers:
>
> (∃x. x) → y
>
> ¬((∃x. x) ∧ ¬y)
>
> ¬(∃x. (x ∧ ¬y))
>
> ∀x.(¬(x ∧ ¬y))
>
> ∀x.(x → y)
>
> I see, this is probably abuse of constructive logic in this case, but I
> believe the idea stays the same.

Yeah, I don't see how this is applicable here.

/Andreas

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

[Dawid Toton]

On 2012-01-11 12:43, rossberg@mpi-sws.org wrote:
> Dawid Toton wrote:
>> Why not to just forbid too general 'a ref types? See the example from
>> the page cited above (with explicit quantifier added):
>>
>> let f : forall 'a. 'a ->  'a =
>>     let r : 'a option ref = ref None in
>>     fun x ->  (* do evil things with the ref cell *)
>>       let y = !r in
>>       let () = r := Some x in
>>       match y with
>>         | None ->  x
>>         | Some y ->  y
>>
>> The problem is that the 'a variable is bound by a general quantifier and
>> at the same time it is used to give a type to the ref cell. But if this
>> were forbidden, I see no need for the value restriction at all. For example:
>>
>> let g : forall 'a. 'a ->  'a =
>>     fun (x : exists 'b. 'b) ->
>>       let r : 'b option ref = ref None in
>>       (* nothing bad can happen *)
>>       ...
> Nothing useful can happen either. You could never read a value back from r
> and use/return it as an 'a or for anything else. So why would you want to
> store it there in the first place?
I can read from r and use it as 'b option. This is useful in general: a 
mutable store can be used locally to speed up computations. I can 
imagine working on 'b array to benefit from fast lookup.
> Also, I don't quite understand how your type annotations are supposed to
> match up. If x : exists 'b. 'b, then f can't be forall 'a. 'a ->  'a.
Use de Morgan's laws for quantifiers:

(∃x. x) → y

¬((∃x. x) ∧ ¬y)

¬(∃x. (x ∧ ¬y))

∀x.(¬(x ∧ ¬y))

∀x.(x → y)

I see, this is probably abuse of constructive logic in this case, but I 
believe the idea stays the same.
Dawid