Programming with ornaments

Journal article

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.

Authors: Ko, H; Gibbons, J

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Cambridge University Press
• Journal: Journal of Functional Programming
• Volume: 27
• Article number: e2
• Publication date: 2016-12-12
• Acceptance date: 2016-10-28
• DOI: 10.1017/S0956796816000307
• EISSN: 1469-7653
• ISSN: 0956-7968