[isabelle-dev] Notes on datatype_new list
makarius at sketis.net
Mon May 26 15:41:04 CEST 2014
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
> 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
More information about the isabelle-dev