[isabelle-dev] Tweak Haskell output for future Haskell compatibility.
makarius at sketis.net
Tue May 8 12:41:46 CEST 2012
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.
More information about the isabelle-dev