[isabelle-dev] Notes on datatype_new list

[Andrei Popescu]

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 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140526/52c604a1/attachment-0002.html>