mutable and polymorphism

mutable and polymorphism

[Radu Grigore]

Compile the following three files one-by-one.
  (*a.ml*) let _ = ref () in let f = fun _ -> () in f 1; f 'a'
  (*b.ml*) let f = let _ = () in fun _ -> () in f 1; f 'a'
  (*c.ml*) let f = let _ = ref () in fun _ -> () in f 1; f 'a'
The files a.ml and b.ml compile; the file c.ml fails with
  Error: This expression has type char
    but an expression was expected of type int
Could someone explain why having a mutable field ("contents" in this
case) restricts the polymorphism of f?

PS: A few hours ago I tried to post from Google Groups, but the
message didn't seem to go thru. Apologies if this is a duplicate

Re: [Caml-list] mutable and polymorphism

[Andreas Rossberg]

On Sep 15, 2010, at 19:10, Radu Grigore wrote:
> Compile the following three files one-by-one.
>  (*a.ml*) let _ = ref () in let f = fun _ -> () in f 1; f 'a'
>  (*b.ml*) let f = let _ = () in fun _ -> () in f 1; f 'a'
>  (*c.ml*) let f = let _ = ref () in fun _ -> () in f 1; f 'a'
> The files a.ml and b.ml compile; the file c.ml fails with
>  Error: This expression has type char
>    but an expression was expected of type int
> Could someone explain why having a mutable field ("contents" in this
> case) restricts the polymorphism of f?

Have a look at this variant of c.ml and its "potential" if it type- 
checked:

>  let f = let xs = ref [] in fun x -> xs := x :: !xs in f 1; f 'a'


/Andreas

Re: [Caml-list] mutable and polymorphism

[Radu Grigore]

On Wed, Sep 15, 2010 at 6:40 PM, Andreas Rossberg <rossberg@mpi-sws.org> wrote:
> Have a look at this variant of c.ml and its "potential" if it type-checked:
>>  let f = let xs = ref [] in fun x -> xs := x :: !xs in f 1; f 'a'

Interesting. If I would be a type checker, here's what I'd do.
1. "ref []" tells me that (xs : '_a), because I know refs can't be polymorphic.
2. "x :: !xs" tells me that (xs : '_a list) and (x : '_a)
3. "x -> x :: !xs" tells me that (f : '_a -> '_a list)
4. "f 1" tells me that (f : int -> int list)
5. "f 'a'" tells me... OOPS

Moreover, I'd have similar thoughts about a variant of a.ml (and a.ml
does typecheck!)
  let xs = ref [] in let f = fun x -> xs:=x::!xs in f 1; f 'a'

On the other hand, here's what I'd do for the original c.ml, which
with a few names added is
  let f = let x = ref () in fun y -> () in f 1; f 'a'
1. "ref ()" tells me that (x : unit ref)
2. "y -> ()" tells me that (f : 'a -> unit)
3. "f 1" returns ()
4. "f 'a'" return ()

In other words, I would have thought that in your example the problem
is that you tried to use a polymorphic reference. (And this problem
even appears in the FAQ.)

regards,
  radu

Re: [Caml-list] mutable and polymorphism

[Goswin von Brederlow]

Radu Grigore <radugrigore@gmail.com> writes:

> On Wed, Sep 15, 2010 at 6:40 PM, Andreas Rossberg <rossberg@mpi-sws.org> wrote:
>> Have a look at this variant of c.ml and its "potential" if it type-checked:
>>>  let f = let xs = ref [] in fun x -> xs := x :: !xs in f 1; f 'a'
>
> Interesting. If I would be a type checker, here's what I'd do.
> 1. "ref []" tells me that (xs : '_a), because I know refs can't be polymorphic.
> 2. "x :: !xs" tells me that (xs : '_a list) and (x : '_a)
> 3. "x -> x :: !xs" tells me that (f : '_a -> '_a list)
> 4. "f 1" tells me that (f : int -> int list)
> 5. "f 'a'" tells me... OOPS
>
> Moreover, I'd have similar thoughts about a variant of a.ml (and a.ml
> does typecheck!)
>   let xs = ref [] in let f = fun x -> xs:=x::!xs in f 1; f 'a'

In your original a.ml you didn't use the reference inside f so f was
polymorphic. That is was then further below the scope of a reference
didn't matter since the application of f was too.

> On the other hand, here's what I'd do for the original c.ml, which
> with a few names added is
>   let f = let x = ref () in fun y -> () in f 1; f 'a'
> 1. "ref ()" tells me that (x : unit ref)
> 2. "y -> ()" tells me that (f : 'a -> unit)

2. "y -> ()" tells me that (f : '_a -> unit)

Because the compiler is stupid and things with a ref can't
polymorphic. It isn't smart enough to see that the type of the ref is
independent of the type of the function and there could remain
polymorphic.

> 3. "f 1" returns ()
> 4. "f 'a'" return ()
>
> In other words, I would have thought that in your example the problem
> is that you tried to use a polymorphic reference. (And this problem
> even appears in the FAQ.)

The solution is called lifting I think?

Anyway, you need to move the polymorphic argument outside the scope of
the reference:

let f y = let x = ref () in (fun y -> ()) y in f 1; f 'a'

> regards,
>   radu

MfG
        Goswin

Re: [Caml-list] mutable and polymorphism

[Radu Grigore]

On Wed, Sep 15, 2010 at 8:10 PM, Goswin von Brederlow <goswin-v-b@web.de> wrote:
> In your original a.ml you didn't use the [...]

Let me rephrase. IMO, both the modified a.ml and the modified c.ml
fail for the same reason: polymorphic references. Therefore, just as
you can't infer from "modified a.ml fails" that "original a.ml should
fail" you can also *not* infer from "modified c.ml fails" that
"original c.ml should fail".

> Because the compiler is stupid and things with a ref can't
> polymorphic.

The compiler isn't stupid: Polymorphic references are unsound. See for
example Section 2.2.3 here:
  http://caml.inria.fr/pub/docs/u3-ocaml/ocaml-core.html#toc8

> let f y = let x = ref () in (fun y -> ()) y in f 1; f 'a'

This has different semantics. Consider
  let f y = let x = ref 0 in (fun y -> incr x) y in f 1; f 'a'

In any case, I'm more interested in an explanation of what happens,
since in practice I'm quite happy with a.ml (together with hiding the
reference from outside by not putting it in mli).

regards,
  radu

Re: [Caml-list] mutable and polymorphism

[Kaustuv Chaudhuri]

On Wed, Sep 15, 2010 at 9:38 PM, Radu Grigore <radugrigore@gmail.com> wrote:
> In any case, I'm more interested in an explanation of what happens,

As you are probably aware, ML-style languages have a so-called "value
restriction" on polymorphism, which in its most vanilla form can be
stated simply as: only values can have a polymorphic type. The
expression

   let x = e in fun y -> ()                                       (1)

is not a value, meaning that it can reduce further, and therefore
the vanilla value restriction says that it cannot have a polymorphic
type.

Now, some very clever people have reasoned that in certain cases the
expression (1) is indistinguishable from a value and by Leibniz's
principle of equality of indistinguishables should therefore be
allowed to have the polymorphic type its equivalent value does.

As an example, one such situation is if e is built from only pure
constructors (i.e., constructors with no mutable fields) and values,
such as:

   let x = () in fun y -> ()

One might even say that (1) should be treated as a value when it
is equivalent to the value expression:

   fun y -> let x = e in ()

There are a number of scenarios in which OCaml can deduce that a
certain non-value expression can have a polymorphic type. For a
comprehensive list of such situations, you can read Jacques Garrigue's
paper on this topic, which also has a great section on the history of
the value restriction [1]. However, OCaml's implementation is
conservative -- it doesn't cover all cases where this fun/let
permutation doesn't change the denotation.

You can easily discover that one kind of expression that OCaml doesn't
allow for this "value-interpretation" of (1) is if e is a function
application. After all, this expression

   let x = infinite_loop () in fun y -> ()

and this:

   fun y -> let x = infinite_loop () in ()

are easily distinguished.

That your function is called "ref" instead of "infinite_loop" is
irrelevant. Mutation is a red herring. You would get the same result
for a completely pure expressions for e; for example:

   # let z = let x = fst (1, 2) in fun y -> () ;;
   val z : '_a -> unit = <fun>

-- Kaustuv

[1] http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.ps.gz

Re: [Caml-list] mutable and polymorphism

[Goswin von Brederlow]

Radu Grigore <radugrigore@gmail.com> writes:

> On Wed, Sep 15, 2010 at 8:10 PM, Goswin von Brederlow <goswin-v-b@web.de> wrote:
>> In your original a.ml you didn't use the [...]
>
> Let me rephrase. IMO, both the modified a.ml and the modified c.ml
> fail for the same reason: polymorphic references. Therefore, just as
> you can't infer from "modified a.ml fails" that "original a.ml should
> fail" you can also *not* infer from "modified c.ml fails" that
> "original c.ml should fail".
>
>> Because the compiler is stupid and things with a ref can't
>> polymorphic.
>
> The compiler isn't stupid: Polymorphic references are unsound. See for
> example Section 2.2.3 here:
>   http://caml.inria.fr/pub/docs/u3-ocaml/ocaml-core.html#toc8

It isn't as smart as you. Call it conservative.

>> let f y = let x = ref () in (fun y -> ()) y in f 1; f 'a'
>
> This has different semantics. Consider
>   let f y = let x = ref 0 in (fun y -> incr x) y in f 1; f 'a'

Yes it does. Which makes the value restriction sometimes anyoing.

> In any case, I'm more interested in an explanation of what happens,
> since in practice I'm quite happy with a.ml (together with hiding the
> reference from outside by not putting it in mli).
>
> regards,
>   radu

Reading up on value restrictions as mentioned in the other mails will
give you the technical details. But they get quite technical so you
might need some background into the theory of functional languages.

MfG
        Goswin

Re: mutable and polymorphism

[Radu Grigore]

Thanks Kaustuv! For whoever may bump into this thread, here's a brief
summary that includes info from
  http://scholar.google.com/scholar?cluster=15692213376116771285
  http://scholar.google.com/scholar?cluster=7879701537639090355

Given (let x = e1 in e2), it is not safe to generalize the type
variables for x when e1 has side-effects. After all e1 performs its
side-effects only once, but a polymorphic type on x may let it be used
as if it does them multiple times. For example,
  let x = ref [] in x := ()::!x; 1::!x
would seem to work if you think about it as
  ref []; (ref [] := () :: !(ref []); 1::!(ref []))
and that's exactly how the type system "thinks" about it if it
generalizes types for x. But, of course, that's not the semantics:
only *one* reference is created at runtime.

Some solutions:
1. Never generalize type variables that appear under ref. (OCaml,
before 1995.) Too restrictive.
2. Keep track of side-effects, for example by using type system
with... effects :). (Many people, before 1995.) The problem is that in
interfaces you need to write types, so you'd need to say whether you
implement something using imperative features or not.
3. Only generalize type variables if e1 clearly doesn't have
side-effects because it's not a computation. (Wright 1995, OCaml up to
3.06.)
4. If it's not clear that e1 doesn't have side-effects, you can still
generalize type variables when they appear only in covariant
positions. (Garrigue 2004, OCaml since 3.07.)

So, in my example
  let f = let x = ref () in fun y -> ()
the type checker finds the type '_a->unit for f, but does not
generalize to 'a->unit because '_a in a contravariant position. On the
other hand, in
  let f = let x = ref [] in fun () -> !x
the type is unit->'_a list so it does generalize.

regards,
  radu

Re: mutable and polymorphism

[Radu Grigore]

I also meant to say...

On Fri, Sep 17, 2010 at 3:04 PM, Radu Grigore <radugrigore@gmail.com> wrote:
> 1. Never generalize type variables that appear under ref.[...]
> 2. Keep track of side-effects, [...]

These are conservative, in the sense that they accept all pure
programs that pass Hindley-Milner.

> 3. Only generalize type variables if e1 [is a value]
> 4. [...] generalize type variables when they appear only in covariant
> positions.

These are *not* conservative.