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

[Lukas Bulwahn]

On 05/08/2012 01:49 PM, Peter Lammich wrote:
> On Di, 2012-05-08 at 12:55 +0200, Tobias Nipkow wrote:
>> 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?
> One use case arises in imperative HOL, where you want to declare
> datatypes that can be stored on the heap, and thus, they only make sense
> if constrained to ::heap - sort. E.g.
>
>
> datatype a'::heap linked_list = nil | node 'a "'a linked_list ref"
>
> Currently, Imperative/HOL does some ML-magic after the datatype
> declarations here, which certainly looks much cleaner when just adding a
> sort constraint.
The mentioned ML-magic achieves two things:
First, you want to restrict 'a to be constrained to heap in the phantom 
type:

datatype ('a :: heap) ref = Ref nat

Second, when defining linked lists, the restriction has to be dropped 
locally,
as "valid" (user-space) type definition would require to prove the 
datatype "'a node" being of sort heap interleaved with its definition in:

datatype 'a node = Empty | Node 'a "('a node) ref"

Maybe with new developments can this be achieved written in a more 
"user-friendly" way, although understanding one line of ML is the least 
problem in the overall confusion of this subject.

It is actually more surprising that sort constraints are imposed 
(however only for convience, and not because of foundational reasons) 
and can be dropped if one wishes at any point.

Lukas

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