Lambda the Ultimate

What this means is that exn is a sum type which you can, with a run-time side-effect, create new branches for. The resemblance to OO comes from the fact that sum types in ML look a bit like classes in OO -- in both cases there's a runtime tag that you can look at. However, there is no subtyping associated with exn.

It's a minor misfeature of ML that the only extensible sum in the language is the one used by the exception mechanism (ie, you can raise exns). These two features (extensible sums and exceptions) are conceptually orthogonal, and should not be coupled.

What makes it a minor rather than serious misfeature is that it's possible to implement the functionality of exn in ML, because ML is pretty much the only language that supports both implicit side effects and true type abstraction.

module type EXTENSIBLE_SUM =
sig
  type tag
  type exn

  type 'a ops = {
    tag : tag;
    make : 'a -> exn;
    case : tag -> exn -> 'a option
  }

  val newtag : unit -> 'a ops
end

module E : EXTENSIBLE_SUM =
struct
  type tag = int
  type exn = tag * (unit -> unit)
  type 'a ops = {
    tag : tag;
    make : 'a -> exn;
    case : tag -> exn -> 'a option
  }

  let gensym =
    let counter = ref 0 in
    fun () -> (incr counter; !counter)

  let newtag () =
    let return = ref None in
    let tag = gensym() in
    let make v =
      (tag, fun () -> return := (Some v)) in
    let case tag' (tag, thunk) =
      let update =
	if tag = tag' then thunk else (fun () -> return := None) in
      (update();
       !return)
    in
    {tag = tag; make = make; case = case}
end

What the module E does is to implement the extensibility features of the exn type. The newtag() operation creates a new branch (identified by a tag), which you can embed values into using the returned make function. Given an exn, you can test whether it has the relevant tag with the case function.

It does this with a bit of higher-order imperative code: morally this exploits the fact that the heap can be viewed as a giant extensible sum type (i.e., where the pointer values are the tags, and the pointed-to object is the tagged data).

They are called "extensible datatypes" or "open sum types" or a combination thereof, see e.g. Harper & Stone's type-theoretic account of SML. There is no subtyping involved, it is essentially just a datatype with an open set of (generative) constructors. (Although there have been proposals for generalizing them to hierarchical datatypes, which does involve subtyping and acts more like a class hierarchy.)

As for languages that support user-defined versions of them: in Alice ML (an SML extension) we allow the users to introduce their own "exttypes", and exceptions just become a special case of that. There are a number of uses for this, e.g. for generative names, to model property lists, or for message types — basically any situation where you need a datatype but there is no single location or module in the program that can/should know all possible variants for it.

So in a language with a module system, like ML, would names for new constructors for these open sum types be module-qualified? If so, that would address most name collision issues. If not, then I'm curious how a name collision would be handled.

Interesting, this "open sum type". Me'thinks me'likes....

I believe open unions and exceptions are not conceptually orthogonal;
their coupling betrays their deep relationship. One may glean that
relationship from using multi-prompt delimited continuations to
implement local exceptions in OCaml (which were not generally possible
in OCaml until a few days ago, when OCaml 3.12 was released):

http://okmij.org/ftp/ML/ML.html#poly-exn

In fact, if a (typed) language supports open unions (in one form or
another) and the continuation monad, the language expresses
multi-prompt delimited continuations. Conversely, any (typed) language
that supports multi-prompt delimited continuations also supports
reference cells, and hence the other forms of open unions.