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

Foundationally nothing, which is why constraints are not present in most 
of the raw definitional primitives, at the bottom of the logic.

There is a difference of the foundation vs. the user context, though. 
(As usual "user" means other packages or end-users connected to the 
surface syntax of such packages.) The Isabelle experts in the background 
have spent countless years to make all this work most of the time, such 
that it is rarely visible now where things actually happen, and how.


 	Makarius