Article contents
Programming with ornaments
Published online by Cambridge University Press: 12 December 2016
Abstract
Dependently typed programming advocates the use of various indexed versions of the same shape of data, but the formal relationship amongst these structurally similar datatypes usually needs to be established manually and tediously. Ornaments have been proposed as a formal mechanism to manage the relationships between such datatype variants. In this paper, we conduct a case study under an ornament framework; the case study concerns programming binomial heaps and their operations — including insertion and minimum extraction — by viewing them as lifted versions of binary numbers and numeric operations. We show how current dependently typed programming technology can lead to a clean treatment of the binomial heap constraints when implementing heap operations. We also identify some gaps between the current technology and an ideal dependently typed programming language that we would wish to have for our development.
- Type
- Articles
- Information
- Copyright
- Copyright © Cambridge University Press 2016
References
- 8
- Cited by
Discussions
No Discussions have been published for this article.