Transporting functions across ornaments

Pierre-Évariste Dagand, Conor McBride

Research output: Contribution to journalArticle

5 Citations (Scopus)
17 Downloads (Pure)

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 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 attempt to reuse code across similarly structured data. In this paper, we capitalise on the structural invariants of datatypes. To do so, we first adapt 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 users can ask the definition of addition to be lifted to lists and they will only be asked the details necessary to carry on adding lists rather than numbers. Our presentation is formalised in the type theory with a universe of datatypes and all our constructions have been implemented as generic programs, requiring no extension to the type theory.
Original languageEnglish
Pages (from-to)316-383
Number of pages68
JournalJournal of Functional Programming
Volume24
Issue number2-3
Early online date23 Apr 2014
DOIs
Publication statusPublished - 30 May 2014
EventICFP 2012 17th ACM SIGPLAN International Conference on Functional Programming - Copenhagen, Denmark
Duration: 10 Sep 201212 Sep 2012

Keywords

  • functional programming
  • correct-by-construction
  • dependent types
  • domain-specific logic
  • inductive families
  • natural number
  • structural invarients
  • structured data
  • type theory

Cite this