Monads and value restriction in ML

The value restriction in ML prevents type generalization in contexts where it could break type safety. The core issue seems to arise from combining sequenced mutation and polymorphic types, as for instance in this OCaml code:

let x = ref [];;  (* value restriction prevents generalization here *)

x := 1::!x;;      (* type unification with int *)
x := true::!x;;   (* error *)

Without the value restriction, the last line would typecheck without error since the polymorphic type for x would unify with bool. To prevent this, the type for x has to remain monomorphic.

My question is the following: would it be possible to remove the value restriction by using monads for expressing sequences of operations?

As function arguments, variables introduced through the monad's bind operation remain monomorphic throughout the whole sequence, so it seems to achieve the same effect as the value restriction without introducing special cases during generalization.

Would this work and if not, why?

Solution

Yes, this basically works, and it's how Haskell does things. However, there's a hitch: you have to make sure the reference never "escapes" the monad. Psuedocode:

module MutMonad : sig
  (* This is all sound: *)
  type 'a t
  type 'a ref

  val mkref : 'a -> ('a ref) t
  val read_ref : 'a ref -> 'a t
  val write_ref : 'a -> 'a ref -> unit t

  (* This breaks soundness: *)
  val run : 'a t -> 'a
end

The existence of run gets us right back where we started:

let x = run (mkref []) in (* x is of type ('a list) ref *)
run (read_ref x >>= fun list -> write_ref (1::list) x);
run (read_ref x >>= fun list -> write_ref (true::list) x)

Haskell gets around this in two ways:

Since main is already a monadic type (IO), it can just not have a runIO or similar.
The ST monad uses a trick with rank 2 types to make sure the references are unusable once the monad exits, allowing locally mutable state while remaining sound.

For the second case you have something like:

module MutMonad : sig
  (* The types now take an extra type parameter 's,
     which is a phantom type. Otherwise, the first
     bit is the same: *)
  type 'a 's t
  type 'a 's ref

  val mkref : 'a -> ('a 's ref) 's t
  val read_ref : 'a 's ref -> 'a 's t
  val write_ref : 'a -> 'a 's ref -> unit 's t

  (* This bit is the key. *)
  val run : (forall 's. 'a 's t) -> 'a
end

The forall 's. ... at the type level is analogous to fun x -> .... 's is bound variable locally, so that the argument to run can't assume anything about 's. In particular, this won't type check:

let old_ref = run (mkref 3) in
run (read_ref old_ref)

Because the arguments to run can't assume that they are passed the same type for 's.

This requires a feature of the type system that doesn't exist in ocaml, and requires a langugae extension (Rank2Types) in Haskell.