Paper Info
Title
An induction principle for nested datatypes in intensional type theory
Abstract
Nested datatypes are families of datatypes that are indexed over all types such that the constructors may relate different family members (unlike the homogeneous lists). Moreover, the argument types of the constructors refer to indices given by expressions in which the family name may occur. Especially in this case of true nesting, termination of functions that traverse these data structures is far from being obvious. A joint paper with A. Abel and T. Uustalu (Theor. Comput. Sci., 333 (1–2), 2005, pp. 3–66) proposed iteration schemes that guarantee termination not by structural requirements but just by polymorphic typing. They are generic in the sense that no specific syntactic form of the underlying datatype “functor” is required. However, there was no induction principle for the verification of the programs thus obtained, although they are well known in the usual model of initial algebras on endofunctor categories. The new contribution is a representation of nested datatypes in intensional type theory (more specifically, in the calculus of inductive constructions) that is still generic and covers true nesting, guarantees termination of all expressible programs, and has an induction principle that allows to prove functoriality of monotonicity witnesses (maps for nested datatypes) and naturality properties of iteratively defined polymorphic functions.
Year
DOI
Venue
2009
10.1017/S095679680900731X
J. Funct. Program.
Keywords
Field
DocType
data structure,type theory,polymorphism,indexation
Data structure,Monotonic function,Expression (mathematics),Algebra,Homogeneous,Computer science,Type theory,Algorithm,Functor,Theoretical computer science,Syntax,Traverse
Journal
Volume
Issue
ISSN
19
3-4
0956-7968
Citations 
PageRank 
References 
9
0.66
19
Authors
1
Name
Order
Citations
PageRank
Ralph Matthes120121.67