Value polymorphism and "generating an exception"

Question

Per The Definition of Standard ML (Revised):

The idea is that dynamic evaluation of a non-expansive expression will neither generate an exception nor extend the domain of the memory, while the evaluation of an expansive expression might.

[§4.7, p19; emphasis mine]

I've found a lot of information online about the ref-cell part, but almost none about the exception part. (A few sources point out that it's still possible for a polymorphic binding to raise Bind, and that this inconsistency can have type-theoretic and/or implementation consequences, but I'm not sure whether that's related.)

I've been able to come up with one exception-related unsoundness that, if I'm not mistaken, is prevented only by the value restriction; but that unsoundness does not depend on raising an exception:

local
  val (wrapAnyValueInExn, unwrapExnToAnyType) =
    let exception EXN of 'a
    in  (EXN, fn EXN value => value)
    end
in
  val castAnyValueToAnyType = fn value => unwrapExnToAnyType (wrapAnyValueInExn value)
end

So, can anyone tell me what the Definition is getting at, and why it mentions exceptions?

(Is it possible that "generate an exception" means generating an exception name, rather than generating an exception packet?)

Answer 1

I'm not a type theorist or formal semanticist, but I think I understand what the definition is trying to get at from an operational point of view.

ML exceptions being generative means that, whenever the control of flow reaches the same exception declaration twice, two different exceptions are created. Not only are these distinct objects in memory, but these objects are also extensionally unequal: we can distinguish these objects by pattern-matching against exceptions constructors.

[Incidentally, this shows an important difference between ML exceptions and exceptions in most other languages. In ML, new exception classes can be created at runtime.]

On the other hand, if your program builds the same list of integers twice, you may have two different objects in memory, but your program has no way to distinguish between them. They are extensionally equal.

---

As an example of why generative exceptions are useful, consider MLton's sample implementation of a universal type:

signature UNIV =
sig
  type univ
  val embed : unit -> { inject : 'a -> univ
                      , project : univ -> 'a option
                      }
end

structure Univ :> UNIV =
struct
  type univ = exn

  fun 'a embed () =
    let
      exception E of 'a
    in
      { inject = E
      , project = fn (E x) => SOME x | _ => NONE
      }
    end
end

This code would cause a huge type safety hole if ML had no value restriction:

val { inject = inj1, project = proj1 } = Univ.embed ()
val { inject = inj2, project = proj2 } = Univ.embed ()

(*  `inj1` and `proj1` share the same internal exception. This is
 *  why `proj1` can project values injected with `inj1`.
 *  
 *  `inj2` and `proj2` similarly share the same internal exception.
 *  But this exception is different from the one used by `inj1` and
 *  `proj1`.
 *  
 *  Furthermore, the value restriction makes all of these functions
 *  monomorphic.  However, at this point, we don't know yet what these
 *  monomorphic types might be.
 *)

val univ1 = inj1 "hello"
val univ2 = inj2 5

(*  Now we do know:
 *  
 *    inj1 : string -> Univ.univ
 *    proj1 : Univ.univ -> string option
 *    inj2 : int -> Univ.univ
 *    proj2 : Univ.univ -> int option
 *)

val NONE = proj1 univ2
val NONE = proj2 univ1

(*  Which confirms that exceptions are generative.  *)

val SOME str = proj1 univ1
val SOME int = proj2 univ2

(*  Without the value restriction, `str` and `int` would both
 *  have type `'a`, which is obviously unsound.  Thanks to the
 *  value restriction, they have types `string` and `int`,
 *  respectively.
 *)