We introduce the notion of identity coercions between non-indexed and indexed variants of inductive datatypes, such as lists and vectors. An identity coercion translates one type to another such that the coercion function definitionally reduces to the identity function. This allows us to reuse vector programs to derive list programs (and vice versa), without any runtime cost. This also allows us to reuse vector proofs to derive list proofs (and vice versa), without the cost of equational reasoning proof obligations. Our work is formalized in Cedille, a dependently typed programming language based on a type-annotated Curry-style type the- ory with implicit (or, erased) products (or, dependent functions), and relies crucially on erasure to introduce definitional equalities between underlying untyped terms.
This paper re-examines the presentation of datatypes in dependently typed languages, addressing in particular the issue of what it means for one datatype to be in various ways more informative than another. Informal human observations like ‘lists are natural numbers with extra decoration’ and ‘vectors are lists indexed by length’ are expressed in a first class language of ornaments — presentations of fancy new types based on plain old ones — encompassing both decoration and, in the sense of Tim Freeman and Frank Pfenning (1991), refinement. Each ornament adds information, so it comes with a forgetful function from fancy data back to plain, expressible as the fold of its ornamental algebra: lists built from numbers acquire the ‘length’ algebra. Conversely, each algebra for a datatype induces a way to index it — an algebraic ornament. The length algebra for lists induces the construction of the paradigmatic dependent vector types. Dependent types thus provide not only a new ‘axis of diversity’ — indexing — for data structures, but also new abstractions to manage and exploit that diversity. In the spirit of ‘the new programming’ (McBride & McKinna, 2004), the engineering of coincidence is replaced by the propagation of consequence. Programming with dependent types is a blessing and a curse. It is a blessing to be able to bake invariants into the definition of datatypes: we can finally write correct-by-construction software. However, this extreme accuracy is also a curse: a datatype is the combination of a structuring medium together with a special purpose logic. These domain-specific logics hamper any effort of code reuse among similarly structured data. In this paper, we exorcise our datatypes by adapting the notion of ornament to our universe of inductive families. We then show how code reuse can be achieved by ornamenting functions. Using these functional ornaments, we capture the relationship between functions such as the addition of natural numbers and the concatenation of lists. With this knowledge, we demonstrate how the implementation of the former informs the implementation of the latter: the user can ask the definition of addition to be lifted to lists and she will only be asked the details necessary to carry on adding lists rather than numbers. Our presentation is formalised in a type theory with a universe of datatypes and all our constructions have been implemented as generic programs, requiring no extension to the type theory.