5
$\begingroup$

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.

Improve this question
$\endgroup$
0

1 Answer 1

Reset to default
5
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ 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. $\endgroup$
    – weakish
    Aug 6, 2017 at 3:38
  • $\begingroup$ @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. $\endgroup$
    – max
    Mar 16 at 15:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.