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

[Makarius]

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