Value restriction

In Hindley–Milner type inference, let x = e1 in e2 generalizes the type of e1 over its free type variables, so that x can be used at different types in e2^[6]. With mutable state this is unsound: if ref [] had type 'a list ref for every 'a, one use could store an int in it and another read a string out of it^[3]. The value restriction, proposed by Wright in 1995^[1] and adopted by Standard ML in 1997^[5], generalizes only syntactic values, since evaluating a value cannot allocate state. It replaced more complex systems of imperative type variables^[3]^[4]. Type variables that cannot be generalized are weak: they stand for one unknown type, fixed by the first use. OCaml generalizes additionally any variable that occurs only in covariant positions, following Garrigue^[2].

§ 01

Example

A value is a constant, a variable, a function, or a constructor applied to values. Anything else is an application.

let r = ref []
let id_list = List.map (fun x -> x)
let id_list' l = List.map (fun x -> x) l
let empty = List.rev []

What ocamlc -i infers.

val r : '_weak1 list ref
val id_list : '_weak2 list -> '_weak2 list
val id_list' : 'a list -> 'a list
val empty : 'a list

The fix for id_list is eta-expansion: adding the parameter back turns the application into a function, which is a value. The last line is the relaxation: 'a appears in the type of empty only as the element type of a list, a covariant position, so it can be generalized even though List.rev [] is an application.

§ 02

Why references cannot be polymorphic

If ref [] were generalized, the same cell could be written at int and read at string. The value restriction leaves its type variable weak, the first write fixes it, and the later read at another type is a type error.

The type rule for let in Damas–Milner inference generalizes over the variables not free in the environment^[6]:

\frac{Γ ⊢ e _{1} : τ _{1} Γ , x : \forall α ˉ . τ _{1} ⊢ e _{2} : τ _{2}}{Γ ⊢ let x = e _{1} in e _{2} : τ _{2}} α ˉ = ftv (τ_{1}) ∖ ftv (Γ)

This is sound for a pure language, where $e_{1}$ denotes the same value however often $x$ is used. When $e_{1}$ allocates a reference, every use of $x$ refers to the same cell, and a polymorphic type for it lets different uses disagree about what it contains. The value restriction adds a side condition: generalize only if $e_{1}$ is a syntactic value; otherwise bind $x : τ_{1}$ with its variables left free^[1].

A weak variable is not an error by itself. It is fixed by the first use that constrains it:

A weak reference and its first use.

let r = ref []
let () = r := [ 1; 2 ]
let first = List.hd !r

What ocamlc -i infers.

val r : int list ref
val first : int

A second use at another type.

let r = ref []
let () = r := [ 1; 2 ]
let () = print_endline (List.hd !r)

The compiler's error.

File "clash.ml", line 3, characters 23-35:
3 | let () = print_endline (List.hd !r)
                           ^^^^^^^^^^^^
Error: This expression has type int but an expression was expected of type
         string

It is an error only if a compilation unit ends with a weak variable still unfixed in its interface, since another unit could then fix it differently^[8].

A module whose only definition is a weak reference.

let r = ref []

The compiler's error.

File "unit.ml", line 1, characters 4-5:
1 | let r = ref []
        ^
Error: The type of this expression, '_weak1 list ref,
       contains type variables that cannot be generalized

§ 03

The unsoundness, concretely

Haskell has no value restriction, because references are created by IO actions and a let cannot run one. unsafePerformIO breaks that separation, and its documentation warns that it can then be used to write a polymorphic reference and so coerce between types^[7].

A polymorphic reference in Haskell.

import Data.IORef
import System.IO.Unsafe (unsafePerformIO)
 
-- A reference created outside IO gets a polymorphic type, exactly what
-- the value restriction forbids in ML.
cell :: IORef [a]
cell = unsafePerformIO (newIORef [])
{-# NOINLINE cell #-}
 
main :: IO ()
main = do
  writeIORef cell [1 :: Int]
  xs <- readIORef cell
  print (head xs :: Double)    -- the Int's bits read as a Double

Running it: the bits of the Int 1, read as a Double.

5.0e-324

This is the program the value restriction rules out in ML.

§ 04

The relaxed value restriction

The restriction rejects many harmless programs, especially partial applications of polymorphic functions. Garrigue observed that a type variable occurring only in covariant positions, such as the element type of an immutable list or the result of a function, cannot be used to store a value of one type and retrieve it at another, since nothing of that type can be passed in^[2]. OCaml therefore generalizes such variables even in applications. For abstract types, the variance must be declared in the signature, with + for covariant or - for contravariant.

The same function behind two signatures, one declaring covariance.

(* Two abstract container types, one declared covariant. *)
module Inv : sig
  type 'a t
  val make : unit -> 'a t
end = struct
  type 'a t = 'a list
  let make () = []
end
 
module Cov : sig
  type +'a t
  val make : unit -> 'a t
end = struct
  type 'a t = 'a list
  let make () = []
end
 
let a = Inv.make ()
let b = Cov.make ()

What ocamlc -i infers.

module Inv : sig type 'a t val make : unit -> 'a t end
module Cov : sig type +'a t val make : unit -> 'a t end
val a : '_weak1 Inv.t
val b : 'a Cov.t

Without the annotation, 'a Inv.t might be a mutable structure, and the type checker must assume the worst.

§ 05

Earlier approaches

Before the value restriction, ML implementations tracked which type variables could reach a reference. Tofte's imperative type variables of 1987–1990 marked variables that might be stored in a reference and refused to generalize them when an expression could allocate^[3], and the Definition of Standard ML of 1990 adopted them; SML of New Jersey used a refinement, weak type variables of numbered strength. Leroy and Weis's closure typing tracked the types of values captured in closures^[4]. These systems accepted more programs, but their types were complicated and exposed implementation details in module signatures. Wright showed that almost all real programs type-check under the simple syntactic restriction, most of the rest after eta-expansion^[1], and Standard ML adopted it in its 1997 revision^[5]. OCaml adopted the relaxed form in version 3.07 in 2003^[2].