<html><body><div style="color:#000; background-color:#fff; font-family:times new roman, new york, times, serif;font-size:14pt">I have a comment followed by a suggestion. <br><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;"><br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">Three years ago when I introduced the concept of BNF, I initially called it "enriched type constructor". <br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">Then people suggested that this name is too unspecific and I came up with "BNF" ("bounded natural functor"), <br>which summarizes the main components: a
natural transformation "set", a cardinal bound, and a functor. This more <br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">specific name however loses an ideological component, namely, my belief that, whenever possible, the first-class citizens <br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">in the type infrastructure of a theorem prover should not be merely operators between types, but "richer items". And a <br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">main argument for this was that datatypes and codatatypes conceptually operate on such richer items, not on type
constructors. <br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">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.) <br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;"><br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">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. </div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;"><br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">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:</div><div class="" style="color:
rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;"><br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">(1) Hide all the extra structure from the user if it is not required explicitly.</div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;"><br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">(2) Make parts of this structure visible upon request by "get" commands that specify the target datatype and the desired <br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new
roman,new york,times,serif; background-color: transparent; font-style: normal;">components, which can be issued at any time (not necessarily immediately) after the datatype definition. Something like:</div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;"><br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">datatype 'a list = Nil | Cons 'a "'a list"</div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;"><br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">...</div><div class=""
style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;"><br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">getSelector isNil for Nil[list]</div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;"><br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">Then novices will first get a chance to experiment with defining their own selectors, set, map, etc. before they are shown <br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif;
background-color: transparent; font-style: normal;">how to get them for free. <br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;"><br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">Andrei <br></div><div class="" style="color: rgb(0, 0, 0); font-size: 18.6667px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;"> <br></div></div></body></html>