> 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
