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

[Peter Lammich]

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.

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