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
___
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.

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 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.

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 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.

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 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.

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 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.

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 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.

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 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.

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 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.

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 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.

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 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.

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 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.

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 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.

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 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.

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 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