[isabelle-dev] Notes on datatype_new list

[Makarius]

On Mon, 26 May 2014, Andrei Popescu wrote:

> 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". main argument for this was that 
> datatypes and codatatypes conceptually operate on such richer items, not 
> on type constructors.

That is a bit hypothetical.  HOL is more or less given as is -- a rather 
boring formal system, but that is also its main strength.  Then everything 
is produced as add-on, without revisiting the foundations over and over 
again, like Type Theory people did in the last 30-40 years (and they are 
still not finished).

Thus the terminology of tools built on top of the basic system naturally 
follows the structure of construction.  A "type" or "type constructor" is 
already defined, so a richer concept needs a new name. I don't see any 
problems with that.  Just plain and simple stacking up of concepts -- even 
though the tool implementations might be very complex.


> 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.)

It remains to be seen when and how homotopy type theory reaches end-users 
of provers like Coq.  I found the talk by Bas Spitters at Rennes 2013 very 
interesting, and usually try to learn more about it, whenever I meet him 
or any other member of this new sect within the Type Theory world.

Revisiting the foundations from scratch also poses technical challanges, 
with unforeseeable impact and canonical delays.  So Coq 8.5 (or later) 
with the magic flag might be ready in 10 days, 10 weeks, or 10 years.


We've had our own upheavals of such a scale in 2006/2007, but it was not 
about foundations, only the immense local theory infrastructure (as 
foundation for locales, interpretation, type classes, class instantiation 
etc.).


 	Makarius