[isabelle-dev] Notes on datatype_new list

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140526/32f6debf/attachment.sig>