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-Systems/universal.ML
David Matthews might actually know more about the history. This idea
has been used in his code base much longer than in Isabelle.
Makarius
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
