Strathprints Home | Open Access | Browse | Search | User area | Copyright | Help | Library Home | SUPrimo

Transporting functions across ornaments

Dagand, Pierre-Evariste and McBride, Conor (2012) Transporting functions across ornaments. [Proceedings Paper]

Full text not available in this repository. (Request a copy from the Strathclyde author)

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 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.

Item type: Proceedings Paper
ID code: 41316
Keywords: dependent types, ornaments, functions, domain-specific logics, transporting functions, Electronic computers. Computer science, Computer Science(all)
Subjects: Science > Mathematics > Electronic computers. Computer science
Department: Faculty of Science > Computer and Information Sciences
Related URLs:
    Depositing user: Pure Administrator
    Date Deposited: 01 Oct 2012 16:11
    Last modified: 27 Mar 2014 11:31
    URI: http://strathprints.strath.ac.uk/id/eprint/41316

    Actions (login required)

    View Item