Polymorphic references

[polymorphism] [mutation]

Polymorphism, as found in ML and Haskell (and in C# and Java where it's called "generics") lets the same definition be reused with multiple different unrelated types. For instance, here's a polymorphic function that creates a single-element list:

let singleton x = [x]
static <A> List<A> singleton(A x) {
    return Arrays.asList(x);

The same singleton function can be used to turn an integer into a list of integers, and also to turn a string into a list of strings.

The standard typing rule for polymorphism is:

Γe:AΓe:α.A if α not free in Γ \frac{Γ ⊢ e : A}{Γ ⊢ e : ∀α . A} \text{ if αα not free in ΓΓ}

That is, if an expression ee has a type AA which mentions a type variable αα, and the type variable αα is used only in the type AA, then the value of ee can be reused with different types substituted for αα. The justification is that different uses of ee can use different types for αα, since nothing outside the type of ee depends on which type is chosen. This process is called generalising the type variable αα.

But if ee can allocate mutable state (say, a mutable reference cell, or a mutable array), then different uses of ee can share state:

let r = ref [] in           (* r : ∀ α . α list ref *)
r := [0];                   (* using r as an int list ref *)
print_string (List.hd !r)   (* using r as a string list ref *)
(* Crash! (Well, it would, if the OCaml compiler allowed this) *)

One obvious-but-broken solution is to disallow polymorphism when the type of ee mentions types with mutable state. This doesn't work: because functions can hide types in their closures, the problem occurs even when the type of ee doesn't mention mutable state:

let f =
  let r = ref None in
  fun x ->
    match !r with
    | None -> r := Some x; x
    | Some x -> x
(* The value restriction means f is not polymorphic,
   but if it were then this would crash: *)
let _ =
  let _ = f 42 in
  print_string (f "hello")

This problem originated in the ML family of languages, as these were the first to combine mutable references and polymorphism. A related problem appeared in Standard ML of New Jersey's implementation of call/cc1, which like mutable references allows multiple uses of an expression to share state (by sharing the continuation). Recently, an instance of this problem arose in OCaml, due to an incorrect typechecker refactoring2. The problem has also appeared in Elm3, using channels to provide the shared mutable state.

(* Counterexample by Bob Harper and Mark Lillibridge *)
fun left (x,y) = x;
fun right (x,y) = y;

let val later = (callcc (fn k =>
	(fn x => x,
         fn f => throw k (f, fn f => ()))))
	print (left(later)"hello world!\n");
	right(later)(fn x => x+2)
(* Counterexample by Thierry Martinez *)
let f x =
  let ref : type a . a option ref = ref None in
  ref := Some x;
  Option.get !ref

let () = print_string (f 0)
-- Counterexample by Izaak Meckler
import Signal
import Html
import Html.Attributes(style)
import Html.Events(..)
import Maybe

c = Signal.channel Nothing

s : Signal Int
s = Signal.map (Maybe.withDefault 0) (Signal.subscribe c)

draw x =
  [ onClick (Signal.send c (Just "I am not an Int"))
  , style [("width", "100px"), ("height", "100px")]
  [ Html.text (toString (x + 1)) ]
  |> Html.toElement 100 100

main = Signal.map draw s

There are several solutions:

  • Separate pure and effectful types

    The original solution chosen in Standard ML distinguishes applicative type variables from imperative type variables. Only applicative variables can be generalised, and only imperative variables can be used in the type of mutable references. There are several variants of this system, from Tofte's original one to extensions used in SML/NJ by MacQueen and others. Greiner4 has a survey of the variants.

    This approach has the disadvantage that internal use of mutation cannot be hidden: a polymorphic sorting function that internally uses temporary mutable storage cannot be given the same type as one that does not.

    Leroy and Weis5 propose a related approach that avoids generalising type variables that may be used in mutable references, without needing to distinguish two classes of type variables. However, to avoid the issue above of functions hiding types in their closure, their solution must distinguish two different sorts of function type according to whether their closure may contain mutable references.

  • The value restriction

    A simpler solution was proposed by Wright6 and is now used in most implementations of ML: generalisation of an expression's type only happens if the expression is a syntactic value, a class that contains e.g. function definitions and tuple constructions, but not function calls or anything that could possibly allocate a mutable reference.

    This solution is much simpler than the type-based approaches, but in some cases less powerful: notably, a partial application of a curried function cannot be generalised without manually eta-expanding.

    In effect, this is also the solution used by e.g. Java and C#: in these languages, only methods may be given generic types, not fields. This ensures that generalisation only occurs on function definitions.

  • Effect typing

    Type-and-effect systems have a typing judgement Γe:A!ΔΓ ⊢ e : A, !, Δ, where ΔΔ is the effect, representing effects that occur as part of evaluating ee. The typing rule for polymorphism in such systems can generalise a type variable αα only if it does not appear in ΓΓ or ΔΔ. If allocating a new mutable reference of type TT results in an effect mentioning TT appearing in ΔΔ, then polymorphic mutable references cannot be created.

  • Effect marking

    Instead of a full-blown type-and-effect system, polymorphic mutable references can be avoided using a type-level marker on computations that may perform any effects at all, and then disabling polymorphism on effectful computations.

    This is the approach taken by Haskell with its monadic encoding of effectful computations in the type IO a. Values of this type represent "IO actions" - computations that, when performed, yield results of type a, possibly causing some side-effects as well. Polymorphism is available as usual when constructing IO actions, but the type of an IO action's result (as used in do notation or via monadic combinators) cannot be generalised. Haskell's do notation for monadic computation does support a let syntax, but its typing is quite different from ordinary let, and it does not allow introducing polymorphism even with an explicit annotation.

    This mechanism allows Haskell to distinguish the following two types:

    good :: forall a . IO (IORef (Maybe a))
    bad  :: IO (forall a . IORef (Maybe a))

    Here, good is an IO action which allocates a mutable reference of an arbitrary type (fine, implementable as newIORef Nothing), while bad is an IO action which allocations a polymorphic mutable reference (unsound). Note that the only distinction between these two is the placement of IO.

    This reliance on marking IO is why Haskell's unsafePerformIO is actually unsafe, as it can be used to strip the IO marker and create polymorphic mutable references:

    import Data.IORef
    import System.IO.Unsafe
    badref :: IORef (Maybe a)
    badref = unsafePerformIO (newIORef Nothing)
    main = do
      writeIORef badref (Just 42)
      Just x <- readIORef badref
      putStrLn (x 1)

ML with callcc is unsound (TYPES mailing list) Bob Harper and Mark Lillibridge (1991)


Weak Polymorphism Can Be Sound, John Greiner (1996)


Polymorphic type inference and assignment, Xavier Leroy and Pierre Weis (1991)


Simple Imperative Polymorphism, Andrew Wright (1995)