On Tue, 8 May 2012, Tobias Nipkow wrote:
I mean the datatype definition facility.
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.)
Kudos to the experts, but my question was *why* the type constraints are
supported for dataypes. What is the use case?
I did not find these ancient mails in my folders from the mid-1990-ies on
the spot. In a private mail to Stefan Berghofer from April 1998, I
mention the problem of passing sort constraints cleanly through datatype
definitions casually, as something that is already known to be supported
(based on earlier discussions with users of the earlier datatype package).
Anyway, without any special expertise in software archeology, a quick
survey of the reachable applications of Isabelle2012 reveals this:
(line 16 of "~~/src/HOL/HOLCF/Up.thy")
datatype 'a u = Ibottom | Iup 'a -- "'a::cpo per default"
(line 428 of "~~/src/HOL/Nitpick_Examples/Manual_Nits.thy")
datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a
aa_tree"
There are several more of the latter kind in AFP, e.g. Collections and
Binomial-Heaps. I did not run the full AFP.
This low frequency of usage is what I also remember over the years. More
frequent issues happen when packages are built in top of other packages
that attempt to disregard the standard treatment of sort constraints in
Isabelle. It is also why I did the renovations last winter, because I had
to explain some users in Fall historical peculiarities of HOL datatypes
that were not really necessary.
One also needs to understand that the foundational part of the package is
the smaller one. There are many add-ons, including a general datatype
interpretation mechanism, where users can define and prove further things
on top of the datatypes. This complexity is the deeper reason why the
datatype package is still only half localized.
So apart from the observation that the foundational kernel does not
require sort constraints (apart from HOL.type of course), were there any
reasons against them?
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
