Programming with ornaments. (12th December 2016)

• Record Type: Journal Article
• Authors: KO, HSIANG-SHANG; GIBBONS, JEREMY
• Is Part Of: Journal of functional programming. Volume 27(2017)
• Publication Date: 2016-12-12
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796816000307
• Languages: English
• ISSNs: 0956-7968

Abstract

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.