The value restriction

Question

In OCaml you can't generalize a partially-applied curried function (the "value restriction").

What is the purpose of the value restriction? What unpleasant would happen if it did not exist?

Trek

Answer 1

Without the value restriction or other mechanisms to restrict generalization, this program would be accepted by the type system:

let r = (fun x -> ref x) [];; (* this is the line where the value restriction would trigger *)

> r : 'a list ref

r := [ 1 ];;

let cond = (!r = [ "foo" ]);;

The variable r would have type 'a list ref, meaning that its contents could be compared to [ "foo" ] although it contained a list of integers.

See Xavier Leroy's PhD thesis for more motivation (ref is not the only construct one may want to add to pure lambda-calculus that introduces the problem) and a survey of the systems that existed at the time of his thesis (including his).

Sair

@Trek The unpleasantness about the solution used in modern OCaml is that if you write purely functional OCaml, the value restriction still applies to you, when it wouldn't need to (your programs are safe by virtue of being purely functional). Some of the systems described in X.L.'s thesis do not have this drawback, but have the drawback of revealing in the types implementation details of the values. As modularization appeared to be the next big thing, the solution that simplified modularization was chosen. Old versions of Caml-light have implemented the system in X.L.'s thesis… – Sair

… which is one of the most sophisticated and (I am pretty sure) allows to type all purely functional Caml programs. You would have to go back to a very old Caml-light version though. As you say, if you want to write purely functional programs, use Haskell. The next version of Haskell will be strict anyway. – Sair

@Trek Look for it in cs.nott.ac.uk/~gmh/appsem-slides/peytonjones.ppt : The next Haskell will be strict, and the next ML will be pure. – Sair

@ThePiercingPrince, don't be too happy ;). First, Haskell has the monomorphism restriction, which is almost the same as the value restriction, except that it only applies when there are class constraints. Second, and worse, unsafePerformIO actually introduces the very same problem that the value restriction is meant to solve in ML. That is, with unsafePerformIO you can write an unsound generic cast function in Haskell, and make hell break loose. – Contraceptive

The reason OCaml having value restriction is it allows mutable? – Lum

@AndreasRossberg but as an orthogonal axis of tradeoffs, isn’t the problem originating from global type inference and thus an alternative which could retain the modularity and eliminate the restrictions would be to annotate the types of all free variables of closures, as apparently Scala requires? – Aziza

@ShelbyMooreIII, no, the problem is independent of type inference. You can easily change the snippet in the answer to a version that is fully annotated and does not even introduce a new function value: let f : 'a. 'a -> 'a ref = ref let r : 'a. 'a list ref = f [] ... That would still blow up if you allowed it. – Contraceptive

@AndreasRossberg, thanks but afaics I’m still correct because ref (is an implicit function that) forms a closure over its input thus must have its specialized type annotated, thus 'a is not allowed as an annotation per my rule? Apologies I presumed you would read the linked post where I had explained that (probably with the incorrect terminology). My intuition originated from attempting to understand why Scala doesn’t have a value restriction even though it’s also call-by-value, given you only contrasted ML vs. Haskell. – Aziza

@ShelbyMooreIII, I'm not sure what you mean. Why would 'a not be allowed as an annotation? How would you then have polymorphism at all? As for Scala, I believe the value restriction is hardwired into its syntax already, because it doesn't even have syntax to define a polymorphic value that is not a function. – Contraceptive

@AndreasRossberg, after sleeping…Scala doesn’t unify covariant List[A] with a GLB ⊤ assigned to List[Int], bcz afaics in subtyping “biunification” the direction of assignment matters. Thus None must have type Option[⊥] (i.e. Option[Nothing]), ditto Nil type List[Nothing] which can’t accept assignment from an Option[Int] or List[Int] respectively. So the value restriction problem originates from directionless unification and global biunification was thought to be undecidable until the recent research linked above. – Aziza

@AndreasRossberg, apology [my comment](#comment84176376_22507665) about ref was discombobulated (age 52 years, working 24 hours w/o sleep) as it doesn’t even form a closure. So my original intuition was apparently worthy in that the value restriction dilemma originates from a typing unification issue, yet I conflated a direct relationship to global inference. Instead apparently due to Hindley-Milner-based non-directional unification— typically indirectly associated with global type inference. Ty helping me distill this! So subtyping might maintain modular encapsulation w/o value restriction! – Aziza

@ShelbyMooreIII, I think you are conflating various things here, such as semantics vs implementation (unification) and parametric polymorphism vs subtyping. But I can't tell for sure. Let me reiterate again that the need for the value restriction is completely independent of whether a language has type inference or not and whether the algorithmic implementation of a type checker uses unification or not. Any language with both parametric polymorphism and references will have to make sure that impure expressions cannot be polymorphic, and the value restriction is a simple condition to ensure so. – Contraceptive

@AndreasRossberg, I may still be wrong, but I’m thinking now that the generative essence is that HM doesn’t model subtyping and polymorphic data types have subtyping invariants which HM can’t model directly thus requiring the invariants to be enforced via value restriction, so that now removes the dependence on unification for implementation. I also made a Q&A on this to get more insight from others. Apologies my inquiry wasn’t better distilled from the start. – Aziza

@ShelbyMooreIII, no, subtyping is irrelevant to the problem. Whether you also add subtyping to the language or not, you still must restrict polymorphic definitions in the same manner. You can merely weaken the restriction to contravariant quantification, see Garrigue's paper on relaxing the value restriction. – Contraceptive

@AndreasRossberg I further explained my dissent at the Q&A I created, and may I suggest perhaps we should move any further discussion there, since we’re being warned here to move extended discussion to chat. Very appreciative of the feedback. – Aziza

Answer 2

Here is the answer I gave some time ago about F#; the issue is exactly the same with OCaml. The problem is that without it, we would be able to create references that point to the wrong type of data:

let f : 'a -> 'a option =
    let r = ref None in
    fun x ->
        let old = !r in
        r := Some x;
        old

f 3           // r := Some 3; returns None : int option
f "t"         // r := Some "t"; returns Some 3 : string option!!!

Tallulah

Answer 3

There is a nice description of weakly polymorphism here(side-effects-and-weak-polymorphism).

Basically, let's take a look at the function below (caching the first ever value it sees):

# let remember =
    let cache = ref None in
    (fun x ->
       match !cache with
       | Some y -> y
       | None -> cache := Some x; x)
  ;;
val remember : '_a -> '_a = <fun>

As it involves imperative, value restriction is applied.

---

However, let's assume there was no value restriction.

Then its type becomes val remember : 'a -> 'a = <fun>.

---

If I now do let () = remember 1, 1 is recorded inside cache, right?

If I call for 2nd time, let x = 3 + remember 2, this should work, because 3 is integer, remember returns the same type as its argument. I am giving 2 here, so remember returns integer too (but value is 1 as we already remembered once). This should pass the type check.

---

What if I call for 3rd time as let y = 3.0 + remember 2.0? Will it work again?

According to remember's type and the reason behind my 2nd call, it also should work, because I am giving float to remember, and it should return float.

But because the first time it already stored 1 (integer) inside, it will return 1 which is an integer. So the type check will fail, right?

---

We can see that without value restriction or weakly polymorphism, due to the mutability is allowed, the whole type check will have trouble. In the silly case above, you need constantly manually check or keep track of what's the initial type remember stored.

Lum