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

[Tobias Nipkow]

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

Kudos to the experts, but my question was *why* the type constraints are
supported for dataypes. What is the use case?

Tobias

> 
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev