Value restriction

In programming languages that combine

• polymorphism
• state, or perhaps even some other effects,
• call-by-value evaluation order
  a certain issue arises. Consider the following OCaml code:

let r = ref [] in      (* generalise r : forall a. a list ref *)
  r := [ () ];         (* specialise a := unit *)
  true :: !r;          (* specialise a := bool *)

If we implement Hindley-Damas-Milner polymorphism naively, then r would have type a list ref for all a. Then, by assigning a list containing the unit value to it, we would specialise it, leading to unsoundness in future uses, like the last line.

To avoid this, languages in the ML family enforce a value restriction: type variables are only generalised (forall a) only in values. For example, ref [] above is not a value, so it would not be generalised.

In algebraic effects and handlers

In languages with polymorphism and algebraic effects and handlers no value restriction is needed Kammar and Pretnar 2017. This leads Kammar and Pretnar to '... conjecture that it is impossible to simulate full-blown reference cells using effect handlers without other language features.'

References

• There appears to be a textbook discussion of this in TAPL - reference to be found.

• Wikipedia page

• An early reference to this in the literature appears in the following paper:

@article{harper_1993,
	title = {Polymorphic type assignment and {CPS} conversion},
	volume = {6},
	doi = {10.1007/BF01019463},
	pages = {361--379},
	number = {3},
	journaltitle = {{LISP} and Symbolic Computation},
	author = {Harper, Robert and Lillibridge, Mark},
	date = {1993}
}

• The observation that no value restriction is required in algebraic effects and handlers is explained in

@article{kammar_2017,
	title = {No value restriction is needed for algebraic effects and handlers},
	volume = {27},
	doi = {10.1017/S0956796816000320},
	journaltitle = {Journal of Functional Programming},
	author = {Kammar, Ohad and Pretnar, Matija},
	date = {2017},
}