Re: [isabelle-dev] Notes on datatype_new list
I can only agree with what Makarius has observed but would go one step further: the new definition of list is truly baroque and unsuitable for beginners, but beginners are bound to look at it. Sometimes languages have to reduce complexity to cater for novices. The three types bool, nat and list should be defined in the plain standard manner. Tobias On 23/05/2014 23:39, Makarius wrote: The following is relevant to the BNF guys, with continously growing team strength (according to Isabelle/aa7f051ba6ab). Today we've had a tutorial with mostly fresh users, which is always useful to see remaining snags. There were also 2-3 experienced Coq users, who have the usual problems of a different kind: being stuck to Emacs or using strange Window managers like Xmonad. Examples for beginners usually use the list datatype, and the Prover IDE makes it easy to find its definition. Many users started looking in the HOL theories routinely, to get an idea how things are defined and how proofs are done with them. Navigation makes the sources more accessible and raises the demands for their quality. (I have ocasionally cleaned up typical hyperlink target positions in Pure, to make them look more obvious, if users happen to enter there.) For the new high-end BNF version of 'a list there were a few funny effects. (1) Its definition looks terrific: datatype_new (set: 'a) list (map: map rel: list_all2) = =: Nil (defaults tl: []) ([]) | Cons (hd: 'a) (tl: 'a list) (infixr # 65) It means it can no longer serve as example template for your own datatype definitions. Note that I have already put the independent Seq.thy example in a prominent place some years ago, to decouple basic examples from the particularly difficult List.thy. (2) Some users somehow used the hd and tl selector specifications above as suggestion to define primitive recursive functions, e.g. like this: primref foo where foo [] = ... | foo (Cons hd tl) = ... Of course this fails, since these are constants, not variables. It results in type-inference errors that beginners find hard to understand, and the Prover IDE has no position information about type errors yet. (3) A genuine name space problem: list is concealed, and thus cannot be completed in semantic completion. Looking briefly through the sources, I merely found some odd workarounds in BNF_Util.typedef -- it is usually worth investing the time to sort out the fine points that lead to such complications and eliminate them: (*TODO: is this really different from Typedef.add_typedef_global?*) 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] Notes on datatype_new list
On 26/05/2014 10:30, Tobias Nipkow wrote: The three types bool, nat and list should be defined in the plain standard manner. Ignore the bit about bool and nat. Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
Am 26.05.2014 um 10:30 schrieb Tobias Nipkow nip...@in.tum.de: I can only agree with what Makarius has observed but would go one step further: the new definition of list is truly baroque and unsuitable for beginners, but beginners are bound to look at it. Sometimes languages have to reduce complexity to cater for novices. I have been careful to distinguish in my email between what the package provides and the syntax it gives for it. Would it be possible to articulate your criticism more precisely along those axes? Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
The definition of list should look like before. Tobias On 26/05/2014 10:59, Jasmin Christian Blanchette wrote: Am 26.05.2014 um 10:30 schrieb Tobias Nipkow nip...@in.tum.de: I can only agree with what Makarius has observed but would go one step further: the new definition of list is truly baroque and unsuitable for beginners, but beginners are bound to look at it. Sometimes languages have to reduce complexity to cater for novices. I have been careful to distinguish in my email between what the package provides and the syntax it gives for it. Would it be possible to articulate your criticism more precisely along those axes? Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
Am 26.05.2014 um 11:02 schrieb Tobias Nipkow nip...@in.tum.de: The definition of list should look like before. I don't see how this is an option. This would result in the following duplicate constants: map_list vs. map set_list vs. set rel_list vs. forall_list2 un_Cons1 vs. hd un_Cons2 vs. tl Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
Am 26.05.2014 11:07, schrieb Jasmin Blanchette: Am 26.05.2014 um 11:02 schrieb Tobias Nipkow nip...@in.tum.de: The definition of list should look like before. I don't see how this is an option. This would result in the following duplicate constants: map_list vs. map set_list vs. set rel_list vs. forall_list2 un_Cons1 vs. hd un_Cons2 vs. tl Here are some compromise options that lighten the presentation, but still reusing the conveniences provided by the package (which are not only the constants, but also many theorems about the constants): (a) datatype_new 'a list = Nil (defaults un_Cons2: []) ([]) | Cons 'a 'a list (infixr # 65) abbreviation map ≡ map_list abbreviation set ≡ set_list abbreviation list_all2 ≡ rel_list abbreviation hd ≡ un_Cons1 abbreviation tl ≡ un_Cons2 (b) datatype_new 'a list = Nil (defaults tl: []) ([]) | Cons (hd: 'a) (tl: 'a list) (infixr # 65) abbreviation map ≡ map_list abbreviation set ≡ set_list abbreviation list_all2 ≡ rel_list Option (a) is closest to the original definition---the only difference is in the annotation defining the default value of tl Nil. However, not using the selector requires us to use the automatically generated name un_Cons2, which makes this option too obscure. My favourite (next to the current definition from the repository) is option (b)---giving name to the selectors makes the defaults annotation easy to parse. And even major functional programming languages support similar selector annotations (e.g. via record syntax for data in Haskell). For both options we probably would change the package to generate the discriminator %x. x = Nil by default for nullary constructors. Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:
(3) A genuine name space problem: list is concealed, and thus cannot
be completed in semantic completion.
I presume you are referring to the fact that
@{const_name Cons} = List.list.Cons
@{const_name hd} = List.list.hd
@{const_name map} = List.list.map
@{const_name rec_list} = List.list.rec_list
where the list component is optional. This behavior is deliberate --
this is what the old package did with all the constants it defined. In
other words,
The only novelty is that we followed the same idiom for the other
constants introduced by the package, such as hd and map.
(This is the easy part of this thread.)
I fully agree with this uniform additional qualification -- it is mainly
for internal robustness.
The observed here problem is different: the type constructor list
somehow ends up in the name space with a concealed flag. There might be
one or more Binding.conceal too many in the BNF sources.
I should probably issue some warning or special PIDE markup whenever a
plain name given in user space is resolved to some concealed entity.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
I have no particular stake in this issue, but I would think there was an option (c) which is to do the *opposite* of what Jasmin said about bringing the additional constant names etc as close as possible to wherever they fit: datatype_new 'a list = Nil ([]) | Cons 'a 'a list (infixr # 65) with set: set rel: list_all2 map: map selectors: hd tl (default []) for Cons hd tl discriminator: op = [] Or something like that, excuse my made-up syntax. That clarifies what the datatype really is and where the associated constants came from (well, a little bit) without having to introduce any funny syntax to fit all the relevant options into a single bit of syntax. It also keeps all the data in a single command, so the package can do everything with the canonical names at once. That's just my ten cents worth. As I said, I have no particular interest in this. Cheers, Thomas. On 26/05/14 19:56, Dmitriy Traytel wrote: Am 26.05.2014 11:07, schrieb Jasmin Blanchette: Am 26.05.2014 um 11:02 schrieb Tobias Nipkow nip...@in.tum.de: The definition of list should look like before. I don't see how this is an option. This would result in the following duplicate constants: map_list vs. map set_list vs. set rel_list vs. forall_list2 un_Cons1 vs. hd un_Cons2 vs. tl Here are some compromise options that lighten the presentation, but still reusing the conveniences provided by the package (which are not only the constants, but also many theorems about the constants): (a) datatype_new 'a list = Nil (defaults un_Cons2: []) ([]) | Cons 'a 'a list (infixr # 65) abbreviation map ≡ map_list abbreviation set ≡ set_list abbreviation list_all2 ≡ rel_list abbreviation hd ≡ un_Cons1 abbreviation tl ≡ un_Cons2 (b) datatype_new 'a list = Nil (defaults tl: []) ([]) | Cons (hd: 'a) (tl: 'a list) (infixr # 65) abbreviation map ≡ map_list abbreviation set ≡ set_list abbreviation list_all2 ≡ rel_list Option (a) is closest to the original definition---the only difference is in the annotation defining the default value of tl Nil. However, not using the selector requires us to use the automatically generated name un_Cons2, which makes this option too obscure. My favourite (next to the current definition from the repository) is option (b)---giving name to the selectors makes the defaults annotation easy to parse. And even major functional programming languages support similar selector annotations (e.g. via record syntax for data in Haskell). For both options we probably would change the package to generate the discriminator %x. x = Nil by default for nullary constructors. Dmitriy ___ 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] Notes on datatype_new list
Am 26.05.2014 11:46, schrieb Tobias Nipkow:
On 26/05/2014 11:07, Jasmin Blanchette wrote:
Am 26.05.2014 um 11:02 schrieb Tobias Nipkow nip...@in.tum.de:
The definition of list should look like before.
I don't see how this is an option. This would result in the following duplicate
constants:
map_list vs. map
set_list vs. set
rel_list vs. forall_list2
un_Cons1 vs. hd
un_Cons2 vs. tl
Duplicate constants are not a killer argument per se. But why not generate those
constants only if the definer asks for them explicitly?
Let's distinguish between A = {hd, tl} and B = {map, set, rel}. The
constants from B are an integral part of the package---they form
together with the type a BNF. Thus, they will always be generated. The
question is whether they are exposed to the user.
The selectors (A) indeed belong in the category of syntactic sugar, and
we have an option to not generate those constants. Here, the question is
about the default behaviour.
Does any programming
language give you all of them by default? Have you made a study of existing
Isabelle datatypes to see how frequently people defined their own
map/set/rel/selectors?
We did not make a global study. But let me pick a random example 'a
rexp from your Regular_Set AFP entry. The theory used to define both
the set function (for atoms) and the map function (for generating marked
regular expressions IIRC). Defining those functions are essentially
boring bureaucracy (each taking 7 lines, not to mention the theorems one
needs to prove about them). In the development version of the AFP, I
changed those to be generated by the new package, saving some lines of
code and allowing the reader to focus on more interesting constants.
The relator is in my experience slightly less user-relevant but it
constitutes an important bridge to the Lifting and Transfer tools.
Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
Just to be clear on this: the ability to get all of these functions for free is
marvellous! We are now discussion only the syntactic interface to that
marvellous functionality, how much is exposed by default, and in particular in
the defn of list.
Tobias
On 26/05/2014 12:14, Dmitriy Traytel wrote:
Am 26.05.2014 11:46, schrieb Tobias Nipkow:
On 26/05/2014 11:07, Jasmin Blanchette wrote:
Am 26.05.2014 um 11:02 schrieb Tobias Nipkow nip...@in.tum.de:
The definition of list should look like before.
I don't see how this is an option. This would result in the following
duplicate constants:
map_list vs. map
set_list vs. set
rel_list vs. forall_list2
un_Cons1 vs. hd
un_Cons2 vs. tl
Duplicate constants are not a killer argument per se. But why not generate
those
constants only if the definer asks for them explicitly?
Let's distinguish between A = {hd, tl} and B = {map, set, rel}. The constants
from B are an integral part of the package---they form together with the type
a
BNF. Thus, they will always be generated. The question is whether they are
exposed to the user.
The selectors (A) indeed belong in the category of syntactic sugar, and we
have
an option to not generate those constants. Here, the question is about the
default behaviour.
Does any programming
language give you all of them by default? Have you made a study of existing
Isabelle datatypes to see how frequently people defined their own
map/set/rel/selectors?
We did not make a global study. But let me pick a random example 'a rexp
from
your Regular_Set AFP entry. The theory used to define both the set function
(for
atoms) and the map function (for generating marked regular expressions IIRC).
Defining those functions are essentially boring bureaucracy (each taking 7
lines, not to mention the theorems one needs to prove about them). In the
development version of the AFP, I changed those to be generated by the new
package, saving some lines of code and allowing the reader to focus on more
interesting constants.
The relator is in my experience slightly less user-relevant but it constitutes
an important bridge to the Lifting and Transfer tools.
Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
On Sun, 25 May 2014, Jasmin Christian Blanchette wrote: The = as the name for Nil's discriminator deserves an explanation. [...] So I introduced this weird = syntax, which suggests that equality is used for discriminating. I am open to other suggestions. The other funky syntax we have is -:. E.g. datatype_new (-: 'a) list = ... This says: Don't generate a set function for 'a -- and don't allow nesting through lists. Just on the squiggles in isolation: if these are rare add-on options one could invent long / explicit keywords for them (or Parse.literal items). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
Let's distinguish between A = {hd, tl} and B = {map, set, rel}. The constants
from B are an integral part of the package---they form together with the type
a BNF. Thus, they will always be generated. The question is whether they
are exposed to the user.
Well, they necessarily need to be exported to the user, because they appear (1)
in the induction principle, (2) in the recursor, and (3) in the prim(co)rec
specifications of any users.
We've been working for three years on the BNF packages and, as much as
possible, have kept everybody fully informed about our plans and intentions, on
this mailing lists, in the documentation, in weekly meetings in Munich, and in
various papers. The constants from B are not only an integral part of the
package, they will be exposed to the user.
The selectors (A) indeed belong in the category of syntactic sugar, and we
have an option to not generate those constants. Here, the question is about
the default behaviour.
Indeed, this is really just a matter of default behavior. Instead of
no_discs_sels, we could have a discs_sels option. But it would make sense
to use it for lists.
Does any programming language give you all of them by default?
ML, Isabelle, and Haskell gives them for records by default. Records are the
non-recursive, single-constructor case of datatypes.
Scala non-scealed case classes also give them to you, e.g.
case class Person(firstName: String, lastName: String)
val me = Person(Daniel, Spiewak)
val first = me.firstName
val last = me.lastName
Have you made a study of existing
Isabelle datatypes to see how frequently people defined their own
map/set/rel/selectors?
The real motivation for discriminators and selectors was codatatypes. For
datatypes, the opinions are more varied -- which is why I made it an option.
However, I did observe that most heavily used datatypes, in Isabelle or ML or
Haskell, tend to have discriminators and selectors, in addition to case. This
includes list and option.
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
Am 26.05.2014 12:25, schrieb Makarius: On Sun, 25 May 2014, Jasmin Christian Blanchette wrote: The = as the name for Nil's discriminator deserves an explanation. [...] So I introduced this weird = syntax, which suggests that equality is used for discriminating. I am open to other suggestions. The other funky syntax we have is -:. E.g. datatype_new (-: 'a) list = ... This says: Don't generate a set function for 'a -- and don't allow nesting through lists. Just on the squiggles in isolation: if these are rare add-on options one could invent long / explicit keywords for them (or Parse.literal items). grep gives 371 occurences of -: in IsaFoR's development repository. So it's not a rare add-on, but an important performance optimization. Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
What new users see when they look at the actual definition of lists is not that important. There are many, many situations where the actual definition of something is much more complicated than the idealised version that one would use for teaching. What is necessary is that simple-looking definitions of the old style still continue to work. In most cases, the simple form is all that will be necessary. I have almost never found destructors or discriminators to be useful. --lcp On 26 May 2014, at 11:21, Tobias Nipkow nip...@in.tum.de wrote: Just to be clear on this: the ability to get all of these functions for free is marvellous! We are now discussion only the syntactic interface to that marvellous functionality, how much is exposed by default, and in particular in the defn of list. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
On Mon, 26 May 2014, Dmitriy Traytel wrote: Just on the squiggles in isolation: if these are rare add-on options one could invent long / explicit keywords for them (or Parse.literal items). grep gives 371 occurences of -: in IsaFoR's development repository. So it's not a rare add-on, but an important performance optimization. If it is only an optimization it is conceptually still rare. But of course it is also possible to invent short keywords -- after some empricial studies about the danger of clashing with common identifiers. The datatypes manual calls the above dead so that is an obvious choice to try out. The BNF package has a slight tendency to cryptic shortcuts to conceal it from outsiders (like category theory in general). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
Am 26.05.2014 12:53, schrieb Makarius: On Mon, 26 May 2014, Dmitriy Traytel wrote: Just on the squiggles in isolation: if these are rare add-on options one could invent long / explicit keywords for them (or Parse.literal items). grep gives 371 occurences of -: in IsaFoR's development repository. So it's not a rare add-on, but an important performance optimization. If it is only an optimization it is conceptually still rare. But of course it is also possible to invent short keywords -- after some empricial studies about the danger of clashing with common identifiers. The datatypes manual calls the above dead so that is an obvious choice to try out. Yes, we have considered this naming earlier. It was discarded, because it looks like one is giving the name dead to a set function. The same holds for any other identifier (not only the common ones). That was the reason to use something that is not an identifier. Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
Am 26.05.2014 um 12:25 schrieb Makarius makar...@sketis.net: On Sun, 25 May 2014, Jasmin Christian Blanchette wrote: The = as the name for Nil's discriminator deserves an explanation. [...] So I introduced this weird = syntax, which suggests that equality is used for discriminating. I am open to other suggestions. The other funky syntax we have is -:. E.g. datatype_new (-: 'a) list = ... This says: Don't generate a set function for 'a -- and don't allow nesting through lists. Just on the squiggles in isolation: if these are rare add-on options one could invent long / explicit keywords for them (or Parse.literal items). Right, let's get the squiggles out of the way. For =:, let's make this the default, so that no keyword is needed. Andreas L. argued against, but it's easy to override by providing a name, and the two main datatypes in Isabelle/HOL, list and option, both use it. For -:, this is indeed a rare add-on option (but an important one to some people). Also, the single worst aspect of the current list definition -- the =: syntax -- could be changed so that this is the default. (It used to be.) Am 26.05.2014 um 13:41 schrieb Dmitriy Traytel tray...@in.tum.de: Yes, we have considered this naming earlier. It was discarded, because it looks like one is giving the name dead to a set function. The same holds for any other identifier (not only the common ones). That was the reason to use something that is not an identifier. Right. On the other hand, it's hard to imagine anybody giving the name dead to the set of values associated with a so called *live* type variable, so perhaps it's not too bad a choice. Also, I agree with Makarius that it is a rare optimization. IsaFoR is a very atypical application (and in fact most of the 371 occurrences could be avoided without changing anything, because deadness is inherited when composing BNFs). Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
Am 26.05.2014 um 12:05 schrieb Makarius makar...@sketis.net: The observed here problem is different: the type constructor list somehow ends up in the name space with a concealed flag. There might be one or more Binding.conceal too many in the BNF sources. Ah, now I get it. Of course this is entirely accidental, and I'm surprised we didn't notice before. We'll look into this. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
I have a comment followed by a suggestion. Three years ago when I introduced the concept of BNF, I initially called it enriched type constructor. Then people suggested that this name is too unspecific and I came up with BNF (bounded natural functor), which summarizes the main components: a natural transformation set, a cardinal bound, and a functor. This more specific name however loses an ideological component, namely, my belief that, whenever possible, the first-class citizens in the type infrastructure of a theorem prover should not be merely operators between types, but richer items. And a main argument for this was that datatypes and codatatypes conceptually operate on such richer items, not on type constructors. I think the other provers should follow our example and take this approach. (I guess homotopy type theory is already taking this approach to some extent, although they may not know about our work.) I beg to disagree with Larry concerning the usefulness of the extra structure beyond expressive (co)datatypes. Whereas working with the destructor or the constructor view is a matter of taste, the other (more fundamental) BNF components, namely set, map, and relator, are *almost always* required in a larger development, and the users end up defining them by hand, issuing a lot of boilerplate (as Dmitriy pointed out). I am willing to bring empirical evidence for this by making a study on Isabelle theories, as well as on theories in other provers. This being said, I see there is a point in keeping the definitions as simple as possible (although I think the set and map functions are instructive even for novices). I have the following proposal: (1) Hide all the extra structure from the user if it is not required explicitly. (2) Make parts of this structure visible upon request by get commands that specify the target datatype and the desired components, which can be issued at any time (not necessarily immediately) after the datatype definition. Something like: datatype 'a list = Nil | Cons 'a 'a list ... getSelector isNil for Nil[list] Then novices will first get a chance to experiment with defining their own selectors, set, map, etc. before they are shown how to get them for free. Andrei ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
Am 26.05.2014 um 14:28 schrieb Andrei Popescu uuo...@yahoo.com: I have the following proposal: (1) Hide all the extra structure from the user if it is not required explicitly. (2) Make parts of this structure visible upon request by get commands that specify the target datatype and the desired components, which can be issued at any time (not necessarily immediately) after the datatype definition. Something like: datatype 'a list = Nil | Cons 'a 'a list ... getSelector isNil for Nil[list] Then novices will first get a chance to experiment with defining their own selectors, set, map, etc. before they are shown how to get them for free. Do I understand you correctly that you are volunteering to implement this?? I wish you good luck, to derive theorems like sel_map etc. on a per-need basis. It's certainly doable, but would be an architectural nightmare. Seriously: We've had a discussion after lunch. We haven't agreed on a concrete syntax, but some elements have emerged: 1. The squiggles (-: and =:) are easy to get rid of, and we'll kill them. This has been discussed before. 2. We'll try to move (map: ... rel: ...) out of the way, e.g. by putting them after the definition rather than before. 3. Similar story for the set function (set: 'a), even though it's a bit painful in the general case (with, say, ten type variables and five mutually recursive types -- cf. IsaFoR). 4. The selector syntax seems acceptable to most of not all parties. Some of us even love it. Also important is that readers are usually smart enough to infer, from the names of the things, what is meant (e.g. hd and tl for a list have to be the selectors). 5. The discriminators are a bit more iffy, and could perhaps be labeled more clearly, e.g. with a pseudo-keyword discriminator. On the other hand, they're not needed for list and option, and the default name (is_C for constructor C) is good. 6. The default values for, e.g. tl [] = [], could be specified as equations after the definition (e.g. in a where clause), as suggested one year ago by Andreas L. One scheme that appeared promising as a compromise is to specify replacement names at the end of the definition, e.g. with map := map_list set := set_list list_all2 := rel (* ugly name BTW -- maybe*) This scales gracefully to the mutual case. I'll do step 1 now, and we can give ourselves more time to think about 2 to 6. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
On Mon, 26 May 2014, Jasmin Blanchette wrote: Am 26.05.2014 um 13:41 schrieb Dmitriy Traytel tray...@in.tum.de: Yes, we have considered this naming earlier. It was discarded, because it looks like one is giving the name dead to a set function. The same holds for any other identifier (not only the common ones). That was the reason to use something that is not an identifier. Right. On the other hand, it's hard to imagine anybody giving the name dead to the set of values associated with a so called *live* type variable, so perhaps it's not too bad a choice. This is presently Parse.reserved (i.e. a plain identifier) followed by a colon. Thus it conforms to similar method section syntax like (simp add: ...) I think you could afford an actual keyword for the dead modifier and use it without colon, like lazy in HOLCF/domain. That would substract dead from the normal identifier space, but merely means its very few occurrences on AFP/Jinja and AFP/JinjaThreads need to be quoted. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
Am 26.05.2014 um 15:24 schrieb Makarius makar...@sketis.net: I think you could afford an actual keyword for the dead modifier and use it without colon, like lazy in HOLCF/domain. That would substract dead from the normal identifier space, but merely means its very few occurrences on AFP/Jinja and AFP/JinjaThreads need to be quoted. Indeed, that would make sense. And perhaps we don't even need to make it a keyword? It shouldn't be hard to parse (dead 'a) with Parse.reserved for dead. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
On Mon, 26 May 2014, Andrei Popescu wrote: Then people suggested that this name is too unspecific and I came up with BNF (bounded natural functor), which summarizes the main components: a natural transformation set, a cardinal bound, and a functor. This more specific name however loses an ideological component, namely, my belief that, whenever possible, the first-class citizens in the type infrastructure of a theorem prover should not be merely operators between types, but richer items. main argument for this was that datatypes and codatatypes conceptually operate on such richer items, not on type constructors. That is a bit hypothetical. HOL is more or less given as is -- a rather boring formal system, but that is also its main strength. Then everything is produced as add-on, without revisiting the foundations over and over again, like Type Theory people did in the last 30-40 years (and they are still not finished). Thus the terminology of tools built on top of the basic system naturally follows the structure of construction. A type or type constructor is already defined, so a richer concept needs a new name. I don't see any problems with that. Just plain and simple stacking up of concepts -- even though the tool implementations might be very complex. I think the other provers should follow our example and take this approach. (I guess homotopy type theory is already taking this approach to some extent, although they may not know about our work.) It remains to be seen when and how homotopy type theory reaches end-users of provers like Coq. I found the talk by Bas Spitters at Rennes 2013 very interesting, and usually try to learn more about it, whenever I meet him or any other member of this new sect within the Type Theory world. Revisiting the foundations from scratch also poses technical challanges, with unforeseeable impact and canonical delays. So Coq 8.5 (or later) with the magic flag might be ready in 10 days, 10 weeks, or 10 years. We've had our own upheavals of such a scale in 2006/2007, but it was not about foundations, only the immense local theory infrastructure (as foundation for locales, interpretation, type classes, class instantiation etc.). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
On Mon, 26 May 2014, Jasmin Blanchette wrote: Am 26.05.2014 um 15:24 schrieb Makarius makar...@sketis.net: I think you could afford an actual keyword for the dead modifier and use it without colon, like lazy in HOLCF/domain. That would substract dead from the normal identifier space, but merely means its very few occurrences on AFP/Jinja and AFP/JinjaThreads need to be quoted. Indeed, that would make sense. And perhaps we don't even need to make it a keyword? It shouldn't be hard to parse (dead 'a) with Parse.reserved for dead. In principle yes. The final answer is left to the one who goes to the bottom of the system to implement it -- and sees if there are other side-conditions. Note that in PIDE there is extra markup even for certain quasi-keywords, e.g. the add in (simp add: ...). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
On Mon, 26 May 2014, Andrei Popescu wrote: getSelector isNil for Nil[list] BTW, camelCaseIsNotUsedInIsabelleSourcesToImproveReadability. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
Am 26.05.2014 um 12:34 schrieb Lawrence Paulson l...@cam.ac.uk: What new users see when they look at the actual definition of lists is not that important. There are many, many situations where the actual definition of something is much more complicated than the idealised version that one would use for teaching. Indeed, this is an old observation that has been repeated over and over throughout the history of computing. The definitions of most library functionality in various programming languages looks obfuscated. Take for example stdio.h in C. On my user-friendly Mac, it looks like this: __BEGIN_DECLS void clearerr(FILE *); int fclose(FILE *); ... int fgetpos(FILE * __restrict, fpos_t *); char*fgets(char * __restrict, int, FILE *); #if defined(_DARWIN_UNLIMITED_STREAMS) || defined(_DARWIN_C_SOURCE) FILE*fopen(const char * __restrict, const char * __restrict) __DARWIN_ALIAS_STARTING(__MAC_10_6, __IPHONE_3_2, __DARWIN_EXTSN(fopen)); #else /* !_DARWIN_UNLIMITED_STREAMS !_DARWIN_C_SOURCE */ FILE*fopen(const char * __restrict, const char * __restrict) __DARWIN_ALIAS_STARTING(__MAC_10_6, __IPHONE_2_0, __DARWIN_ALIAS(fopen)); #endif /* (DARWIN_UNLIMITED_STREAMS || _DARWIN_C_SOURCE) */ int fprintf(FILE * __restrict, const char * __restrict, ...) __printflike(2, 3); In Lisp, I'd like to see how they define nil, cons, car, cdr, and cadadaar. Even staying with Isabelle, all types defined before 'a list and 'a option are good examples -- products, sums, nats, unit, bools are all defined in a terrible way. Now, with jEdit allowing to jump to the definition (as opposed to the documentation), I can see that this becomes a more acute issue Yet again I would argue that the terrific and truly baroque specification of list is better than products, sums, nats, unit, bools. I have almost never found destructors or discriminators to be useful. I'd be curious to understand why. Perhaps you could elaborate in a separate thread. With multiple constructor datatypes, it is true that one often ends up needing a case expression anyway, but there are still many situations where you need the discriminator (or a '=' or '~=' that amounts to one) in an assumption, and then it's convenient to use the selectors directly, e.g.: lemma rotate1_hd_tl: xs \noteq [] \Longrightarrow rotate1 xs = tl xs @ [hd xs] Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Notes on datatype_new list
Hi all, many issues have been touched in this thread, but I would like to get back to the proposals made by Jasmin which IMHO point into the right direction. 1. The squiggles (-: and =:) are easy to get rid of, and we'll kill them. This has been discussed before. OK. No need to discuss this any longer. 2. We'll try to move (map: ... rel: ...) out of the way, e.g. by putting them after the definition rather than before. This corresponds to the pattern »start with the main clause, put the adverbial after«. Very good. In after-2007 Isar, there is also a tendency to be more verbose in statements, avoiding too many implicit positional arguments: with map := map_list set := set_list list_all2 := rel (* ugly name BTW -- maybe*) instead of something like »(map set list_all2)« 3. Similar story for the set function (set: 'a), even though it's a bit painful in the general case (with, say, ten type variables and five mutually recursive types -- cf. IsaFoR). Same argument: it is easier to understand a (natural language) sentence if there are not too many interjections before the main predicate. 4. The selector syntax seems acceptable to most of not all parties. Some of us even love it. Also important is that readers are usually smart enough to infer, from the names of the things, what is meant (e.g. hd and tl for a list have to be the selectors). I have no strong opinion about that. But the side discussion whether to prefer »head« and »tail« seems also fruitful to avoid confusion. 5. The discriminators are a bit more iffy, and could perhaps be labeled more clearly, e.g. with a pseudo-keyword discriminator. On the other hand, they're not needed for list and option, and the default name (is_C for constructor C) is good. I have a slight feeling that syntax for selectors and discriminators should be corresponding. 6. The default values for, e.g. tl [] = [], could be specified as equations after the definition (e.g. in a where clause), as suggested one year ago by Andreas L. This is more verbose to parse, but it also quite common in Isar to require propostions of a certain shape instead of (conceptually isomorphic) fragments. A similar example are mixin equations in interpretation statements. So far. 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] Notes on datatype_new list
Hi again, datatype_new 'a list = Nil (defaults un_Cons2: []) ([]) | Cons 'a 'a list (infixr # 65) abbreviation map ≡ map_list abbreviation set ≡ set_list abbreviation list_all2 ≡ rel_list abbreviation hd ≡ un_Cons1 abbreviation tl ≡ un_Cons2 this would make sense if you were to abandon the lhses in favour of the rhses in the mid future, which, as I dare to state plainly, you don't want to do. Duplication is a migration solution, not a solution in itself. 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
