Re: [isabelle-dev] Tweak Haskell output for future Haskell compatibility.
Hi Bertram, just a curious question: in which context are you using the Isabelle code generator? CU, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Tweak Haskell output for future Haskell compatibility.
This is an interesting issue. I would like to know if we need class constraints
for datatype parameters in the first place. I thought we had agreed at some
point (not on this list) to get rid of them, but we never did. Maybe there are
situations where you need them? The only one that comes to my mind is the
following: you define some type ('a::C) t by a typedef and then make it into a
datatype by hand (via rep_datatype). Now you can use it inside a datatype
definition. Do we have a (conceivable) example of this situation?
Tobias
Am 07/05/2012 16:02, schrieb Bertram Felgenhauer:
Dear Isabelle developers,
the Haskell code generator of Isabelle currently emits contexts for
data and newtype generates, e.g. (from CeTA):
newtype (Linorder a) = Rbt a b = Rbt (Rbta a b);
The sole effect of such contexts is that the programmer must provide
a (Linorder a) context wherever Rbt a b is used, which is fairly uselss.
In the next version of the Haskell language definition (whenever that
will be), this feature will be removed.
http://www.haskell.org/pipermail/haskell-prime/2011-January/003335.html
http://hackage.haskell.org/trac/haskell-prime/wiki/NoDatatypeContexts
Ghc currently requires a flag (-XDatatypeContexts) to compile code
using datatype contexts. In the latest release (7.4.1), this option
emits a warning:
Warning: -XDatatypeContexts is deprecated: It was widely considered a
misfeature, and has been removed from the Haskell language.
I propose, therefore, to omit these contexts in code generated by
Isabelle. This can safely wait until after the release, of course.
(patch attached)
Best regards,
Bertram
This body part will be downloaded on demand.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Tweak Haskell output for future Haskell compatibility.
On Tue, 8 May 2012, Tobias Nipkow wrote:
This is an interesting issue. I would like to know if we need class
constraints for datatype parameters in the first place. I thought we had
agreed at some point (not on this list) to get rid of them, but we never
did. Maybe there are situations where you need them? The only one that
comes to my mind is the following: you define some type ('a::C) t by a
typedef and then make it into a datatype by hand (via rep_datatype). Now
you can use it inside a datatype definition. Do we have a (conceivable)
example of this situation?
Are you speaking about the actual definitional package, or its adjoined
code-generator?
In ancient times, the datatype package did not treat sort constraints at
all. It was not required for the logical foundations of the construction,
and it was not yet clear how to write such packages properly. I.e. all
the now standard ways of processing input, type-checking it, passing
around parameters etc. were not yet established.
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.)
There was additional confusion in packages built on top of datatype,
because of incompatibilities of the way its input is specified. We have
spent many years to reform all this, to keep the datatype package
up-to-date. I've made the last reforms in the Christmas vacation
2011/2012, so that the NEWS for Isabelle2012 can now say:
* Datatype: type parameters allow explicit sort constraints.
This is only a trivial consequence of straightening, clarifying,
simplifying all the internal layers of these packages.
Of course, the code generator can ignore sort constraints on its own,
without affecting any of the specification packages.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Tweak Haskell output for future Haskell compatibility.
Am 08/05/2012 12:01, schrieb Makarius:
On Tue, 8 May 2012, Tobias Nipkow wrote:
This is an interesting issue. I would like to know if we need class
constraints for datatype parameters in the first place. I thought we had
agreed at some point (not on this list) to get rid of them, but we never did.
Maybe there are situations where you need them? The only one that comes to my
mind is the following: you define some type ('a::C) t by a typedef and then
make it into a datatype by hand (via rep_datatype). Now you can use it inside
a datatype definition. Do we have a (conceivable) example of this situation?
Are you speaking about the actual definitional package, or its adjoined
code-generator?
I mean the datatype definition facility.
In ancient times, the datatype package did not treat sort constraints at all.
It was not required for the logical foundations of the construction, and it
was
not yet clear how to write such packages properly. I.e. all the now standard
ways of processing input, type-checking it, passing around parameters etc.
were
not yet established.
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?
Tobias
There was additional confusion in packages built on top of datatype, because
of
incompatibilities of the way its input is specified. We have spent many years
to reform all this, to keep the datatype package up-to-date. I've made the
last
reforms in the Christmas vacation 2011/2012, so that the NEWS for Isabelle2012
can now say:
* Datatype: type parameters allow explicit sort constraints.
This is only a trivial consequence of straightening, clarifying, simplifying
all
the internal layers of these packages.
Of course, the code generator can ignore sort constraints on its own, without
affecting any of the specification packages.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Tweak Haskell output for future Haskell compatibility.
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Tweak Haskell output for future Haskell compatibility.
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Tweak Haskell output for future Haskell compatibility.
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.) Kudos to the experts, but my question was *why* the type constraints are supported for dataypes. What is the use case? I did not find these ancient mails in my folders from the mid-1990-ies on the spot. In a private mail to Stefan Berghofer from April 1998, I mention the problem of passing sort constraints cleanly through datatype definitions casually, as something that is already known to be supported (based on earlier discussions with users of the earlier datatype package). Anyway, without any special expertise in software archeology, a quick survey of the reachable applications of Isabelle2012 reveals this: (line 16 of ~~/src/HOL/HOLCF/Up.thy) datatype 'a u = Ibottom | Iup 'a -- 'a::cpo per default (line 428 of ~~/src/HOL/Nitpick_Examples/Manual_Nits.thy) datatype 'a aa_tree = \Lambda | N 'a\Colonlinorder nat 'a aa_tree 'a aa_tree There are several more of the latter kind in AFP, e.g. Collections and Binomial-Heaps. I did not run the full AFP. This low frequency of usage is what I also remember over the years. More frequent issues happen when packages are built in top of other packages that attempt to disregard the standard treatment of sort constraints in Isabelle. It is also why I did the renovations last winter, because I had to explain some users in Fall historical peculiarities of HOL datatypes that were not really necessary. One also needs to understand that the foundational part of the package is the smaller one. There are many add-ons, including a general datatype interpretation mechanism, where users can define and prove further things on top of the datatypes. This complexity is the deeper reason why the datatype package is still only half localized. So apart from the observation that the foundational kernel does not require sort constraints (apart from HOL.type of course), were there any reasons against them? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Tweak Haskell output for future Haskell compatibility.
Am 08/05/2012 13:49, schrieb Peter Lammich: datatype a'::heap linked_list = nil | node 'a 'a linked_list ref Actually, I think this does not do what you hope it does, hence the magic is still in there. But Lukas showed me a related defn: datatype 'a ref = Ref nat where 'a is a phantom type but for extra-logical reasons you want to restrict 'a to some type class. Extra-logical reasons can be quite compelling ;-) I'm convinced. Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Tweak Haskell output for future Haskell compatibility.
Am 08/05/2012 14:44, schrieb Makarius: So apart from the observation that the foundational kernel does not require sort constraints (apart from HOL.type of course), were there any reasons against them? They are not allowed in Haskell anymore, so why do we allow them (and complicate the code generation for Haskell in the future)? That was the starting point. That the kernel does not require sort constraints is not the point. Even if it did, you would still not need sort constraints in datatypes because their construction does not involve any sorts. You could always (I think) define an unconstrained datatype, even if its intended usage is in a constrained setting. I now see that there are certain extra-logical uses and accept that some people just like to explicitly constrain the usage of a datatype. Now that the machinery works smoothly, I would not suggest to remove it. Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Tweak Haskell output for future Haskell compatibility.
On Tue, 8 May 2012, Makarius wrote: I did not find these ancient mails in my folders from the mid-1990-ies on the spot. At last, I've found my mail folders before the year 1996. On 29-Sep-1994 someone was pointing out that latest Gofer and Haskell would now support type class constraints in datatypes, observing this as a current trend in functional programming, and demanding that Isabelle/HOL would have to follow :-) This was long before I got myself involved in the datatype package, and we added the support for sort constraints in Stefan's version for other reasons than following other languges trends. I can tell further stories about the domain variant by David von Oheimb, but maybe I should stop the history session here. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Tweak Haskell output for future Haskell compatibility.
On Tue, 8 May 2012, Tobias Nipkow wrote: Am 08/05/2012 14:44, schrieb Makarius: So apart from the observation that the foundational kernel does not require sort constraints (apart from HOL.type of course), were there any reasons against them? They are not allowed in Haskell anymore, so why do we allow them (and complicate the code generation for Haskell in the future)? That was the starting point. The expert(s) on code generation should comment on that, most notably Florian. When he made his first round on the renewed codegenerator, we changed a few things at the bottom of the logic to get sort constraints out of the way. As a consequence, primitive consts and corresponding definitional axioms have become free from sort constraints, but the results are presented to the user with constraints as expected. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Tweak Haskell output for future Haskell compatibility.
Dear Isabelle developers, the Haskell code generator of Isabelle currently emits contexts for data and newtype generates, e.g. (from CeTA): newtype (Linorder a) = Rbt a b = Rbt (Rbta a b); The sole effect of such contexts is that the programmer must provide a (Linorder a) context wherever Rbt a b is used, which is fairly uselss. In the next version of the Haskell language definition (whenever that will be), this feature will be removed. http://www.haskell.org/pipermail/haskell-prime/2011-January/003335.html http://hackage.haskell.org/trac/haskell-prime/wiki/NoDatatypeContexts Ghc currently requires a flag (-XDatatypeContexts) to compile code using datatype contexts. In the latest release (7.4.1), this option emits a warning: Warning: -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language. I propose, therefore, to omit these contexts in code generated by Isabelle. This can safely wait until after the release, of course. (patch attached) Best regards, Bertram # HG changeset patch # User felgenhauer # Date 1336397766 -7200 # Node ID 1a976d546b94ca265a26f6d916a7f54979c0c547 # Parent 29212a4bb866adc5f8f94a85602acb8dbcd65f81 do not generate contexts for datatype declarations in generated Haskell code (see http://hackage.haskell.org/trac/haskell-prime/wiki/NoDatatypeContexts) diff -r 29212a4bb866 -r 1a976d546b94 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Fri May 04 17:12:37 2012 +0200 +++ b/src/Tools/Code/code_haskell.ML Mon May 07 15:36:06 2012 +0200 @@ -57,7 +57,7 @@ | SOME (_, print) = print (print_typ tyvars) fxy tys) | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v; fun print_typdecl tyvars (vs, tycoexpr) = - Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr); + print_tyco_expr tyvars NOBR tycoexpr; fun print_typscheme tyvars (vs, ty) = Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty); fun print_term tyvars some_thm vars fxy (IConst c) = ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
