On Tue, 8 May 2012, Tobias Nipkow wrote:
This is an interesting issue. I would like to know if we need class
constraints for datatype parameters in the first place. I thought we had
agreed at some point (not on this list) to get rid of them, but we never
did. Maybe there are situations where you need them? The only one that
comes to my mind is the following: you define some type "('a::C) t" by a
typedef and then make it into a datatype by hand (via rep_datatype). Now
you can use it inside a datatype definition. Do we have a (conceivable)
example of this situation?
Are you speaking about the actual definitional package, or its adjoined
code-generator?
In ancient times, the datatype package did not treat sort constraints at
all. It was not required for the logical foundations of the construction,
and it was not yet clear how to write such packages properly. I.e. all
the now standard ways of processing input, type-checking it, passing
around parameters etc. were not yet established.
Over the years this lead to occasional confusion of end-users, who wanted
to restrict their datatype constructors on purpose. (I can dig up an
email by Elsa Gunter from the late 1990-ies, if you want.)
There was additional confusion in packages built on top of datatype,
because of incompatibilities of the way its input is specified. We have
spent many years to reform all this, to keep the datatype package
up-to-date. I've made the last reforms in the Christmas vacation
2011/2012, so that the NEWS for Isabelle2012 can now say:
* Datatype: type parameters allow explicit sort constraints.
This is only a trivial consequence of straightening, clarifying,
simplifying all the internal layers of these packages.
Of course, the code generator can ignore sort constraints on its own,
without affecting any of the specification packages.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
