mutable and polymorphism
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Kaustuv Chaudhuri <kaustuv.chaudhuri@i...> 
Subject:  Re: [Camllist] mutable and polymorphism 
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, MLstyle languages have a socalled "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 nonvalue 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 "valueinterpretation" 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/garriguevalue_restrictionfiwflp04.ps.gz