Computability in Europe 2006
Logical Approaches to Computational Barriers

Special Session Talk:
Recursion on Nested Datatypes in Dependent Type Theory

Speaker: Ralph Matthes
Author(s): Ralph Matthes


Nested datatypes are families of datatypes that are indexed over all types and where different family members are related by the datatype constructors. This may be used to represent variable binding or to maintain certain invariants through typing.
In dependent type theory, a major concern is the termination of all expressible programs, so that types that depend on object terms can still be type-checked mechanically. Therefore, we study iteration and recursion schemes that have this termination guarantee throughout, and they are not based on syntactic criteria (recursive calls with "smaller" arguments) but just on types ("type-based termination"). An important concern are reasoning principles that are compatible with the ambient type theory, in our case induction principles.
In previous work, the author has proposed an abstract description of nested datatypes together with a mapping operation (like map for lists) and an iterator on the term side and an induction principle on the logical side that could all be implemented within the Coq system (with impredicative Set that is just needed for the justification, not for the definition and the examples). Of utmost importance is the ability to prove naturality theorems (called "free theorems" by Wadler) for the obtained iterative functions. This has been possible in case studies on "bushes" and representations of lambda terms (also with explicit flattening).
The new contribution is an extension of this abstract description to full primitive recursion and its illustration by way of examples that have been carried out in Coq. Unlike the iterative system, we do not yet have a justification within Coq.

websites: Arnold Beckmann 2008-04-01