Re: [isabelle-dev] Notes on datatype_new list
Hi Florian,
> 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.
Thanks for your comments. The current syntax (as per dc0b4f50e288) is
datatype_new (set: 'a) list (map: map rel: list_all2) =
Nil (defaults tl: "[]") ("[]")
| Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
Moving things to the end could yield something like
datatype_new 'a list =
Nil ("[]")
| Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
where
"hd [] = []"
sets: set
map: map
rel: list_all2
(I got the OK from Tobias for keeping the selectors in there.)
For mutually recursive types, there could be one "where" per type -- but I
doubt that "where" and mutual recursions will often need to be combined anyway.
In the heat of the discussion, we might have forgotten that most datatypes
actually look quite good today, e.g.
datatype_new 'a option =
None
| Some (the: 'a)
>> 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.
Good point. And since the default is reasonable ("= C" for nullary constructors
C, "is_C" otherwise), the syntax is rarely needed. (Andreas uses it for "lnull
:: 'a llist => bool", though.)
>> 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.
Right. It is also easier to parse (and to get right as an author) for
constructors with arguments. See the example right at the end of Section 3 of
http://www21.in.tum.de/~blanchet/co-data-impl.pdf
if you want a taste of how unnatural default values can get. The default for
"mid (Node2 x l r)" is "%x l r. r".
Actually, here I did not need much convincing. My main objection with the
equational scheme was that someone would need to implement it...
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 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
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
On Mon, 26 May 2014, Jasmin Christian Blanchette wrote:
Am 26.05.2014 um 12:34 schrieb Lawrence Paulson :
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);
One could blame the C language for being obsolete and requiring all this
extra rubbish, but even Scala can compete here. Scala libraries are easy
to use, but only a few elect experts know how there are implemented.
See again
http://stackoverflow.com/questions/1722726/is-the-scala-2-8-collections-library-a-case-of-the-longest-suicide-note-in-hist
I've implemented collections myself until Scala 2.7, but starting with
Scala 2.8 I am flying blind, and merely hope to get my own little add-ons
over continued changes by the experts, e.g. see 86f9c6912965.
For HOL we have our own history of complexity in the bootstrap process.
Everything below theory Main might be somehow obscure. Often it is
possible to do some peephole optimizations to reduce the obscurity to a
reasonable level.
The same for Pure. The new @{here} antiquotation at least gives the
formal declaration point of type "fun", but without any clue how it is
really done.
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 26/05/2014 16:13, Jasmin Christian Blanchette wrote: > Am 26.05.2014 um 12:34 schrieb Lawrence Paulson : > >> 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: I disagree. You should not obfuscate definitions that have an equivalent simple version. Makarius spoke from experience when he said that people will look at List.thy and they will get confused. That confusion should be minimized rather than saying that other types (eg nat) are also defined in a terrible way. We would not define them like that if datatype was already there at that point. Tobias > __BEGIN_DECLS > void clearerr(FILE *); > intfclose(FILE *); > ... > intfgetpos(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) */ > intfprintf(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 \ [] \ 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
Am 26.05.2014 um 12:34 schrieb Lawrence Paulson : > 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 \ [] \ 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
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
On Mon, 26 May 2014, Jasmin Blanchette wrote: Am 26.05.2014 um 15:24 schrieb Makarius : 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:
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
Am 26.05.2014 um 15:24 schrieb Makarius : > 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, Jasmin Blanchette wrote: Am 26.05.2014 um 13:41 schrieb Dmitriy Traytel : 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 14:28 schrieb Andrei Popescu : > 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
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 12:05 schrieb Makarius : > 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
Am 26.05.2014 um 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). 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 : > 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 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
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
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 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
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
> 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
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
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 :
>>>
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
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 :
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
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 :
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
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
Am 26.05.2014 11:07, schrieb Jasmin Blanchette:
Am 26.05.2014 um 11:02 schrieb Tobias Nipkow :
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 26/05/2014 11:07, Jasmin Blanchette wrote: > Am 26.05.2014 um 11:02 schrieb Tobias Nipkow : > >> 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? 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? Concerning the selectors: the default names will almost never be what the users wants and hence she will have to mention them anyway (if she wants them). 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 11:02 schrieb Tobias Nipkow : > 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
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 : > >> 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 10:30 schrieb Tobias Nipkow : > 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
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
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
Hi Makarius,
> 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.
Andreas Lochbihler made similar observations to us privately, but about lazy
lists (which are very similar). What makes lists so special is that they have
lots of traditional names and syntaxes, and the very general "datatype_new"
package tries to integrate such a special citizen as best it can.
More precisely, the syntactic complexity stems from these sources:
1. "Mixfix" syntax: [], #
2. BNF artifacts: set, map, list_all2
3. discriminators: (%xs. xs = []) and (%xs. xs ~= [])
4. selectors: hd, tl, and tl [] = []
My claims are:
A. We need to specify all those four things. Strictly speaking, we could pass
the "no_discs_sels" option and not generate any discriminator-and-selector
constants and properties. But since lists have "hd" and "tl" anyway, better
generate them in a uniform way.
B. The concrete syntax tries to put names as close to where they belong. E.g.
the set function "set" is put next to the type argument 'a, the "hd" and "tl"
to the corresponding constructor value, and even the default "tl [] = []" next
to the "Nil" constructor. The map and relator names are close to the type
constructor name "list", which makes sense from a "functorial" point of view.
In sum, I claim the BNF package does the right thing, and that the syntax is
quite convenient and mostly feels natural, but that lists are about the worst
case imaginable.
The "=" as the name for Nil's discriminator deserves an explanation. Without
it, the package would generate an "is_Nil" predicate. But looking in the
existing list theory, I saw that "= []" was the thing that was used to check
for emptiness. I made "= []" be the default for nullary constructors, but
Andreas Lochbihler noticed that this caused some unexpected trouble (at least
for codatatypes) because it mixes the constructor and the destructor views of a
type. 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.
Andrei Popescu pointed to the documentation. The "=" syntax is explained at the
end of Section 2.1 (p. 8 in aa7f051ba6ab). It is curiously lacking in the
reference section Section 2.2.1. I'll add it.
> (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.
In some sense, this is almost a compliment for the package. Instead of giving
arbitrary names to arguments, users now realize that there is a connection
between the arguments and the selectors.
In this particular instance, I think the root of the problem is that "hd" and
"tl" are too short names to serve as good constant names. In Haskell, they call
these "head" and "tail", and given the way parsing works in Isabelle, I would
argue that they would be more suitable.
> (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,
@{const_name Cons} = "List.list.Cons"
@{const_name list_rec} = "List.list.list_rec"
holds with Isabelle2013-2. 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 easy to change: Basically, grepping for "Binding.qualify false" in
"src/HOL/Tools/{Ctr_Sugar,BNF}/*.ML" locates the offenders.
The optional components appear to be a safe guard against duplicate names
across datatypes (or other entities) defined in a single theory. I have no
strong opinion there, except that my clear preference is for a scheme that
treats constructors, discriminators, selectors, set functions, map fu
Re: [isabelle-dev] Notes on datatype_new list
>> datatype_new (set: 'a) list (map: map rel: list_all2) =
>> =: Nil (defaults tl: "[]") ("[]")
>> | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
>> Can you explain the squiggle =: above? I did not find it in the manual
>> nor in the sources so far. It seems to be special to main HOL datatypes.
> what it does is indicate for Nil that a discriminator (of type "'a list =>
> bool")
> should not be provided, but instead equality with Nil should be used.
> This option seems to only be available for nullary constructors.
A couple more notes on this:
The places before the constructor names, like the one before Nil where "=:"
currently stands, can be used to give any discriminator name, as in
datatype_new (set: 'a) list (map: map rel: list_all2) =
myDiscriminatorForNil: Nil (defaults tl: "[]") ("[]")
| Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
which yields myDiscriminatorForNil :: "'a list => bool" together with the
relevant facts.
The default is to generate a discriminator with name built from the
constructor, here is_Nil.
Note however that for lists a discriminator is_Cons is *not* generated unless
the user explicitly
requires one, since the datatype has only two constructors and it is more
convenient to use the negation
of is_Nil instead of is_Cons. However, if the datatype has more than two
constructors, as in
datatype_new (set: 'a) listBlah (map: map rel: list_all2) =
Nil (defaults tl: "[]") ("[]")
| Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
| Blah
then discriminators are produced for all of them: is_Nil, is_Cons, and is_Blah.
Jasmin has polished these to the extreme.
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/doc/datatypes.pdf
Andrei
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Notes on datatype_new list
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
