[isabelle-dev] Notes on datatype_new list

[Jasmin Christian Blanchette]

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