[isabelle-dev] Notes on datatype_new list

[Jasmin Christian Blanchette]

> 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