Transporting Functions across Ornaments

Details Transporting Functions across Ornaments Transporting Functions across Ornaments

2012-01-23

arxiv.org/abs/1201.4801v2

Computer Science

Programming Languages

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

Transporting Functions across Ornaments does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Transporting Functions across Ornaments, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Transporting Functions across Ornaments will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-498313