Refining Inductive Types

Dependently typed programming languages allow sophisticated properties ofdata to be expressed within the type system. Of particular use in dependentlytyped programming are indexed types that refine data by computationally usefulinformation. For example, the N-indexed type of vectors refines lists by theirlengths. Other data types may be refined in similar ways, but programmers mustproduce purpose-specific refinements on an ad hoc basis, developers mustanticipate which refinements to include in libraries, and implementations mustoften store redundant information about data and their refinements. In thispaper we show how to generically derive inductive characterisations ofrefinements of inductive types, and argue that these characterisations canalleviate some of the aforementioned difficulties associated with ad hocrefinements. Our characterisations also ensure that standard techniques forprogramming with and reasoning about inductive types are applicable torefinements, and that refinements can themselves be further refined