# What's the advantage of "value restriction" over its alternatives?

What is the motivation to pick "value restriction" over other candidates?

Examples of alternatives:

1. Enclosing pureness into the function type, for example:

pure_function : x -> x
impure_function : x => x

2. Polymorphism by name (call by name) as in Xavier Leroy, 1993

Xavier Leroy, 1993. Polymorphism by name for references and continuations. In 20th symposium Principles of Programming Languages, pages 220-231. ACM Press, 1993.

I'm sure that this isn't the only advantage, but I think the primary advantage is simplicity. This is even identified in the original paper introducing the value restriction: previous solutions all existed, but the complexity of annotations made them undesirable.

• The majority of value that people want to give polymorphic types are functions, which are values, and you can "fake it" with thunks for anything that isn't a value.
• The language of types is unchanged, so it's easier for the programmer to use. There is no need for extra annotations or types. The users

In "real world" languages, the solutions falls into two categories. ML-style languages use the value restriction, and Haskell-style language use purity and monadic effects. Rust even uses a more restrictive version of the value restriction, where only top-level functions can be polymorphic.

As is common with PL research, there may be many theoretically sound solutions which don't gain traction in popular languages because of their difficulty or awkwardness of use.

• Enclosing pureness into function type only introduces one difference on typing (pure/impure). I believe it is not much more complex than value restriction. In fact value restriction itself does introduce one extra type '_a. Polymorphism by name does not touch the type system at all, and does not need any annotation. It just need a small syntax change as (Leroy, 1993) pointed out. Aug 6, 2017 at 3:38
• @weakish Interesting read, thanks. It seems that the same result may be obtained by shoving refs inside some lazy computation monad (with dereference as a monad escape), so that if the language has a do-notation, no syntax change is even needed.
– max
Mar 16 at 15:41