Transporting Functions across Ornaments

TL;DR

This paper introduces a method to reuse functions across different data types by extending the concept of ornaments to functions, enabling more flexible and correct code reuse in dependently typed programming.

Contribution

It formalizes functional ornaments within a universe of inductive families, allowing code reuse between functions on related data types without extending the type theory.

Findings

Demonstrates how to lift functions like addition to operate on lists.

Provides a formal framework for functional ornamentation in type theory.

Implementation of generic programs for code reuse without extending the type system.

Abstract

Programming with dependent types is a blessing and a curse. It is a blessing to be able to bake invariants into the definition of data-types: we can finally write correct-by-construction software. However, this extreme accuracy is also a curse: a data-type 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 data-types 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 ornament, 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 data-types and all our constructions have been implemented as generic programs, requiring no extension to the type theory.