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

2012-05-13 Thread Florian Haftmann
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

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

2012-05-08 Thread Tobias Nipkow
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

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

2012-05-08 Thread 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

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

2012-05-08 Thread Tobias Nipkow
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

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

2012-05-08 Thread 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

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

2012-05-08 Thread Tobias Nipkow
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

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

2012-05-08 Thread 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

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

2012-05-08 Thread 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

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

2012-05-08 Thread 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.) Kudos

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

2012-05-08 Thread Tobias Nipkow
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

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

2012-05-08 Thread Tobias Nipkow
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

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

2012-05-08 Thread Makarius
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

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

2012-05-08 Thread Makarius
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

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

2012-05-07 Thread 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