[isabelle-dev] New (Co)datatypes: Status & Plan (FYI)

[Jasmin Christian Blanchette]

Dear all,

As you might know, Andrei Popescu, Dmitriy Traytel, and I have been working on a
new (co)datatype package. It is part of Isabelle2013 in the directory
"src/HOL/Tools/BNF" (BNF = bounded natural functors) [1]. The package is
described in some detail in our LICS 2012 paper [2].

The package introduces a pair of commands: "datatype_new" and "codatatype". The
main features are:

  * Support for recursion via well-behaved type constructors (BNFs), e.g. "fset"
  * Support for codatatypes (coinductive datatypes)
  * More modular architecture, allowing mixed (co)recursion
  * Work inside local theories

Interestingly, the first three features are in essence what is mentioned as
future work in Berghofer & Wenzel's TPHOLs '99 paper [3], and the fourth feature
is of course highly desirable.

Our first goal was to bring codatatypes to those who really need them. Thanks to
Andreas Lochbihler's efforts, the AFP entry "Coinductive" and its dependencies
("JinjaThreads" and "Lazy-Lists-II") have now been ported to the new package
(instead of relying on heavy manual constructions).

The next goal is subsume the current "datatype" command. This is to avoid code
duplication, dodge interoperability issues, etc. In particular, it means we
don't have to port the old package to local theories (a big to-do item on
Makarius's list).

There will be a high level of compatibility between the old and the new package.
For nonnested recursive datatypes, compatibility is quasi-100%; and for nested
datatypes, the package will support an optional "nested to mutual" reduction to
simulate the old package, so that the same theorems as before are available
(albeit under different names).

The work has been ongoing for nearly two years and is still in progress. In the
coming weeks, we will integrate "primrec_new" in Isabelle -- it is being
developed in a separate repository, mostly by B.Sc. student Lorenz Panny.
Another important missing piece is "primcorec".

A rough, optimistic time plan follows.

August--September 2013:
    Finish "datatype_new"
      * Finish "primrec_new"
      * Reduce nested recursion to mutual recursion to provide same convenient
        interface as old package (on demand)
      * Automatically register new datatypes as old datatypes so that "fun" etc.
        work seamlessly (for purely inductive datatypes)

    Move "datatype_new" to "HOL-Main"
      (this will add < 30 s to build time, hopefully less)

October--December 2013 (?):
    Release Isabelle2013-1 with both "datatype" and "datatype_new"

Winter 2014:
    Gradually port theories in Isabelle and AFP to "datatype_new"

Spring 2014:
    Rename {"datatype" |-> "legacy_datatype", "datatype_new" |-> "datatype"}

Summer/Fall 2014:
    Release Isabelle2014 with both "legacy_datatype" and "datatype"

Fall 2014:
    Move "legacy_datatype" into "HOL-Library"

Summer 2015 (?):
    Release Isabelle2015 with only "datatype"

Your questions and comments are welcome.

Cheers,

Jasmin (& Andrei & Dmitriy)

[1] http://isabelle.in.tum.de/library/HOL/HOL-Cardinals-Base/HOL-BNF-LFP/README.html
[2] http://www21.in.tum.de/~traytel/papers/lics12-codatatypes/index.html
[3] http://www4.in.tum.de/~berghofe/papers/TPHOLs99.pdf