[isabelle-dev] Tweak Haskell output for future Haskell compatibility.

[Makarius]

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