Value Restriction

There is a problem with mixing impredicative polymorphism, i.e., polymorphism in System F, and side effects, e.g., references, continuations, etc. This problem arises when we allow arbitrary computations to considered polymorphic. The solution usually used is to restrict the programming language so that only values are allowed to be abstracted as polymorphic programs. Here we discuss this issue and its solution which is usually referred to as “Value Restriction”.

These examples are taken from a paper by Wright and Felleisen.¹ This paper also includes an example using exceptions that is not discussed below.

The problem

When an expression has type $\tau$ it means that the expression, when evaluated, produces a value of type $\tau$. If we allow arbitrary expressions to be abstracted into polymorphic programs we can cause problems. Particularly, the program can have side effects and it can be that every time the program is executed it can be with a different side effect with a different type. That is, we can have a program that each time executed produces something of the type $\tau[\sigma/X]$ (type $\tau$ where type variable $X$ is substituted with type $\sigma$) for different $\sigma$’s depending on the side effect. If we declare such a program polymorphic, i.e., of type $\forall X. \tau$, then the program will be executed once and the resulting value will have type $\forall X. \tau$, which means it can be considered to have different types. However, the side effects have already taken place and hence the type should have been fixed!!¹

Example with references

The following piece of code is an illustrative example using references. I use an OCaml-like syntax for examples. Obviously, this code is not well-typed in OCaml which is a type safe language.

  let x : 'a. ('a option) ref = ref None in
  x := Some "A";;
  match !x with
    None -> 5
  | Some y -> y - 3

In this example the computation ref None above is assumed to have a polymorphic type. When this program gets evaluated a reference, say $\ell$, is allocated and x gets bound to it. The reference $\ell$ can now be used as a reference that can store values of type 'a option for any type 'a. This is clearly problematic as we can write Some "A" to $\ell$ and subsequently treat $\ell$ as a reference to int option and read it! Hence, if allowed, the program above would crash when evaluated as it would attempt to evaluate "A" - 3.

Example with continuations (call/cc)

The following piece of code is an illustrative example using continuations. I use an OCaml-like syntax, although OCaml does not directly support continuations (there is library support though). I write call/cc(K. e) where in e the captured current continuations is bound to K. I use the command throw v to K to go back to the captured continuation K with value v. I write out the important types so that the example is easier to read.

  let x : 'a. (('a -> 'a) * (('a -> 'a) -> int)) =
    call/cc (K. (fun x -> x, fun f -> throw (f, fun _ -> 5) to K))
  in
  let f : bool -> bool =
	let (f', _) = x in f'
  in
  let g : (int -> int) -> int =
	let (_, g') = x in g'
  in
  (f (fun x -> x - 3)) (f true)

The typing rules for call/cc and throw are as follows: $$ \frac{\Gamma, K : \mathsf{Cont}(\tau) \vdash e : \tau}{\Gamma \vdash \mathtt{call/cc}(K.~ e) : \tau} \hspace{4em} \frac{\Gamma \vdash e : \mathsf{Cont}(\tau) \hspace{2em} \Gamma \vdash e' : \tau}{\Gamma \vdash \mathtt{throw}~ e' ~\mathtt{to}~ e : \sigma} $$ Here $\mathsf{Cont}(\tau)$ is the type of a captured continuation which can be resumed by giving a value of type $\tau$. The typing rule for throw makes sense because when we throw the program back to a captured continuation, we never return! Hence, a throw expression can have any type necessary. Also, notice that the reason why we separately compute f and g from x is that in each case the polymorphic value x is instantiated at different types; bool for f and int for g.

When evaluated, x will be bound to a pair of functions, let us use f and g to refer to them as does the code above. The function f is simply the identity function, hence, (f true) at the bottom simply reduces to true. However, calling g with the function fun x -> x - 3 goes back to the first line of the code and this time binds x to a pair ((fun x -> x - 3), (fun _ -> 5)). At this point, when we project f out (for the second time now), there is already a problem, it does not really have the type bool -> bool but rather int -> int! Hence, this time, when we get to the point where we evaluate f true we evaluate it to true - 3 at which point the program crashes.

Solution

The solution usually used to solve this problem is called “value restriction”. That is, the language only allows programs to be abstracted as polymorphic values if they are already values. Such programming languages are known to be type safe; see our paper as an example of such a system and its accompanying Coq code for a proof of type safety.² In this paper, all polymorphic programs are marked with $\Lambda$. In our language all programs of the form $\Lambda\;e$, i.e., all polymorphic programs are considered values unless if they are instantiated. This enforces the value restriction.

This requirement can also be relaxed; for example, OCaml considers infers the type of ref None as 'a. ('a option) ref but here 'a is simply a placeholder for a type that is unknown type which is fixed as soon as the value resulting from this expression is used at a specific type. The following is the result obtained using OCaml 4.07.1:

  # let x = ref None in x := Some 3; match !x with None -> 1 | Some y -> y;;
  - : int = 3

Bibliography