Re: [Caml-list] mutable and polymorphism

[Kaustuv Chaudhuri <kaustuv.chaudhuri@inria.fr>]

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