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

[Tobias Nipkow]

Am 08/05/2012 12:01, schrieb 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?
> 

I mean the datatype definition facility.

> 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.)

It is precisely such a convincing example I am looking for. It seems to me that
such constraints restrict the types artificially: the type makes sense without
it. What is gained by the constraint?

Tobias

> 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
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev