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

[Jasmin Blanchette]

Hi Florian,

Am 04.08.2013 um 18:57 schrieb Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

> has an explicit need for a »nested to mutual« mode ever been
> articulated?

Yes, on a couple of occasions. First, as Dmitriy mentioned, compatibility is important -- I certainly don't want to be at the receiving end of emails written by angry Australians. Second, I explicitly asked one of our power users:

>>  to what extent to you agree or disagree with the following claims?
>> 
>>  1. Porting existing old-style specs to the new style is difficult enough, and
>>     the scenario arises often enough, that it would be desirable/necessary for
>>     the new package to support it.
>> 
>>  2. Even for new specifications, the old style is sometimes preferable. Hence it
>>     should be encouraged and fully supported, presumably even for codatatypes.

He or she answered:

> I strongly agree with both. I see an analogy with fold(l/r): Many functions in Isabelle could be defined as folds, but hardly anybody does, because the terms are unreadable once you unfold the definition in a goal. For (co)datatype, the common case of recursion through 'a list in general leads exactly to the foldr definition. And usually, you want different equations than those for foldr for combining the lists. So, you introduce the constant and abstraction and rewrite the equations afterwards.


To avoid heated debates, we want to support both the modular view and the nonmodular view, in all combinations, and also for primcorec. (Moreover, it's an interesting academic challenge; we're not aware of any literature about doing this reduction at the level of (co)recursions and (co)induction principles.)

> Overall, a realistic and reasonable schedule.

Great! I fear the schedule erring on the optimistic side, but in any case do expect some constant progress, because we are not going to give up after two years of work on this.

> Is there any experimental evicdence how many datatype specifications
> would break by a drop-in replacement (real applications, not
> demonstration examples)?  If this is significantly little, I would even
> think about doing the switch {"datatype" |-> "legacy_datatype",
> "datatype_new" |-> "datatype"} immediately.  The »_new« suffix has a
> strange connotation of »almost done… ad multos annos«.

It appears highly desirable to have at least one iteration of official Isabelle release where "datatype_new" is more or less a drop-in replacement for "datatype", so that it gives plenty of time for developers of huge theories (e.g. the Australians) to experiment with it, one type at a time, and give us their feedback.

Another reason for procrastination is that we're getting a bit close to the Isabelle2013-1 release. By the time we're done with "primrec_new" and the nested-to-mutual reduction, we should look into convergence, not divergence.

Dmitriy also mentioned some reasons, related to the need to adapt some infrastructure (e.g. the "interpretation" mechanism, used for "size" and many other extensions).

Finally, there's the performance issue I mentioned in another email regarding n-way mutual recursion for n >= 8 approximately. I'm sure this will bite one or two users at least. We'll need to take a very close look at that, but unlikely before the next release.

Thanks for your interest and comments!

Cheers,

Jasmin