I have a comment followed by a suggestion.
Three years ago when I introduced the concept of BNF, I initially called it
"enriched type constructor".
Then people suggested that this name is too unspecific and I came up with "BNF"
("bounded natural functor"),
which summarizes the main components: a natural transformation "set", a
cardinal bound, and a functor. This more
specific name however loses an ideological component, namely, my belief that,
whenever possible, the first-class citizens
in the type infrastructure of a theorem prover should not be merely operators
between types, but "richer items". And a
main argument for this was that datatypes and codatatypes conceptually operate
on such richer items, not on type constructors.
I think the other provers should follow our example and take this approach. (I
guess homotopy type theory is already taking this approach to some extent,
although they may not know about our work.)
I beg to disagree with Larry concerning the usefulness of the extra structure
beyond expressive (co)datatypes. Whereas working with the destructor or the
constructor view is a matter of taste, the other (more fundamental) BNF
components, namely set, map, and relator, are *almost always* required in a
larger development, and the users end up defining them by hand, issuing a lot
of boilerplate (as Dmitriy pointed out). I am willing to bring empirical
evidence for this by making a study on Isabelle theories, as well as on
theories in other provers.
This being said, I see there is a point in keeping the definitions as simple as
possible (although I think the set and map functions are instructive even for
novices). 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.
Andrei _______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
