Search code examples
polymorphismocaml

The value restriction

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?

Solution

  • 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).