On Tue, 15 Mar 2011, Lucas Dixon wrote:
I'm not sure if this is what you meant, but the type of exceptions is heterogeneous in the sense that all exceptions, no matter what data they hold, have the same type.
The idea is used in Isabelle's generic contexts, among other places.
(btw - does anyone know who came with this idea? I think the first time I saw it was in the Isabelle source code 10 years ago or so...)
This probably refers to my version of it, with the functor wrapping that I made around 1999. It elaborates on much older variants that originated in Cambridge or Edinburgh, IIRC.
The shortest current version of the idea is this clone of the universal type from the Poly/ML internal library:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2011/src/Pure/ML-Syste...
David Matthews might actually know more about the history. This idea has been used in his code base much longer than in Isabelle.
Makarius