[isabelle-dev] Notes on datatype_new list

[Jasmin Christian Blanchette]

Am 26.05.2014 um 14:28 schrieb Andrei Popescu <uuomul at 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140526/152f0b24/attachment-0002.html>