\( \DeclareMathOperator{\tr}{tr} \newcommand\D{\mathrm{d}} \newcommand\E{\mathrm{e}} \newcommand\I{\mathrm{i}} \newcommand\bigOh{\mathcal{O}} \newcommand{\cat}[1]{\mathbf{#1}} \newcommand\curl{\vec{\nabla}\times} \newcommand{\CC}{\mathbb{C}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\ZZ}{\mathbb{Z}} % For +---- metric \newcommand{\BDpos}{} \newcommand{\BDneg}{-} \newcommand{\BDposs}{\phantom{-}} \newcommand{\BDnegg}{-} \newcommand{\BDplus}{+} \newcommand{\BDminus}{-} % For -+++ metric \newcommand{\BDpos}{-} \newcommand{\BDposs}{-} \newcommand{\BDneg}{} \newcommand{\BDnegg}{\phantom{-}} \newcommand{\BDplus}{-} \newcommand{\BDminus}{+} \)
UP | HOME

Value Restriction - SML

Table of Contents

1. Basic Idea

We run into problems when we try to have let-polymorphism with mutable references. This was the subject of Mads Tofte's PhD dissertation back in the 1980s.

The solution first proposed was to distinguish imperative type variables from applicative type variables. This turned out to be a nightmare in practice.

Then Wright discovered that let-expressions usually bind values to local variables, and this would allow us to avoid the problems discussed in Tofte's dissertation. It was adopted in the 1997 Definition of Standard ML (see the use of nonexpansive expressions, which are "syntactical values").

2. References

  • Andrew K. Wright, "Simple imperative polymorphism". LISP and Symbolic Computation 8 no.4 (1995): 343–355. https://doi.org/10.1007/BF01018828.
    • This is the paper which introduced the concept of "value restriction" as a solution to the problem posed by a mutable reference cell type in ML-like languages.
  • Jacques Garrigue, "Relaxing the Value Restriction". pdf, 2004(?)
  • Value Restriction, which summarizes the paper:
    • Amin Timany and Lars Birkedal. "Mechanized relational verification of concurrent programs with continuations". Proc. ACM Program. Lang. 3, ICFP, Article 105 (July 2019), 28 pages. DOI: https://doi.org/10.1145/3341709
  • MLton Wiki

Last Updated 2025-02-25 Tue 18:36.