Re: [Caml-list] Proposal for extensible open datatypes

[Andreas Rossberg <rossberg@mpi-sws.org>]

On Jan 6, 2012, at 07.26 h, Andrej Bauer wrote:
> I would be interested to hear what propeties of Ocaml you had to give
> up to get this interesting extension working? For example, what
> happens with checking for exhaustivness of match? Caml performs
> various optimizations in pattern matching, why are those still ok now
> that new alternatives may appear later?

One such type is already in ML, for historical reasons it happens to  
be named exn. Consequently, you don't really give up anything, your  
questions already apply to the exception type. Exhaustiveness simply  
requires a catch-all in all pattern matches over this type. More  
difficult is irredundancy, because constructors can be aliased without  
the type system tracking that (and it cannot across module  
boundaries). You have to give up there.

Generalising exn this way is an old idea, e.g. we implemented it in  
Alice ML. The standard reply to requesting such an extension is that  
it's not really needed, because you can already do everything using  
exn (though without custom type distinctions, and minus GADTs in OCaml).

/Andreas