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
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.
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.
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.
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 = \ | N "'a\linorder" 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.
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-...@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
___
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] jEdit
On Wed, 2 May 2012, Christian Sternagel wrote: would it make sense to introduce some kind of "read-only" mode for theory files and then use this mode when jumping to a file that is already finished (instead of the "Attempt to update loaded theory ..." error message)? Of course I don't know whether it is easily possible to distinguish between files that are already loaded as part of a heap image and files that are loaded by hand (which should not be loaded in read-only mode). On a related note: the output of such loaded files is still interesting. Is there any way to make the output immediately available from the heap image, without actually loading the theory (in the end it was already loaded when creating the heap image, but I guess the output is a side-effect and not part of the resulting heap)? This all makes sense, and is in the pipe-line for a long time already. It is all about reforming the old theory loader (and its batch mode) to converge it with the interactive document model that is now seen in the Prover IDE. It will probably take a bit more time to get there, extrapolating from the slow progress of the past 4 years. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] print modes
On Wed, 2 May 2012, Brian Huffman wrote:
On Wed, May 2, 2012 at 6:55 AM, Christian Sternagel
wrote:
is it really the case that currently the only way to obtain ASCII output
using print modes is by specifying the empty string, like
thm ("") conjE
or did I miss anything? Since this print mode is occasionally useful, I
suggest to provide a named variant, like 'plain', 'ASCII', or whatever.
The variety of print modes were introduced to overcome certain limitations
of display capabilities. In a sense most of that is "legacy", but I've
recently refurbished the description in the manual, see isar-ref section
7.1.3 in Isabelle2012-RC2. Mode "" is formally the default, the fall-back
print mode.
Anyway, what are your remaining applications for ASCII notation?
I would actually go a bit further, and get rid of "xsymbol" as a special
syntax mode.
It bothers me that if I want to define a constant with both ascii and
symbol notation, I have to use the ascii variant in the actual
definition, and then add the (far more commonly-used) symbol notation
later.
definition foo :: "'a => 'a => bool" (infix "~~" 50) where ...
notation (xsymbol) foo (infix "\" 50)
I would rather write:
definition foo :: "'a => 'a => bool" (infix "\" 50) where ...
notation (ascii) foo (infix "~~" 50)
In some sense "xsymbol" is merely a convention. Nothing stops you from
inventing other print modes on the spot. Is is a matter of library
organization how this is done in practice.
Since plain symbol notation now works most of the time, both in the editor
and in HTML, one could eventually move on to discontinue these special
modes and use more symbols by default.
Then there would be only one (symbol) notation for most things. For very
basic things like !! ==> etc. this would require thoughts, though.
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: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-...@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.
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:
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.
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
