{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:57:12Z","timestamp":1776891432711,"version":"3.51.2"},"reference-count":24,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2016,12,12]],"date-time":"2016-12-12T00:00:00Z","timestamp":1481500800000},"content-version":"unspecified","delay-in-days":346,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2016]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>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 \u2014 including insertion and minimum extraction \u2014 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.<\/jats:p>","DOI":"10.1017\/s0956796816000307","type":"journal-article","created":{"date-parts":[[2016,12,12]],"date-time":"2016-12-12T03:28:25Z","timestamp":1481513305000},"source":"Crossref","is-referenced-by-count":10,"title":["Programming with ornaments"],"prefix":"10.46298","volume":"27","author":[{"given":"HSIANG-SHANG","family":"KO","sequence":"first","affiliation":[]},{"given":"JEREMY","family":"GIBBONS","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2016,12,12]]},"reference":[{"key":"S0956796816000307_ref1","first-page":"61","volume-title":"Proceedings of International Conference on Functional Programming","author":"Bernardy","year":"2013"},{"key":"S0956796816000307_ref18","doi-asserted-by":"crossref","unstructured":"McBride C. (2014) How to keep your neighbours in order. In Proceedings of International Conference on Functional Programming, Manuel M.T. Chakravarty (ed), ICFP'14. New York, NY, USA: ACM, pp. 297\u2013309.","DOI":"10.1145\/2628136.2628163"},{"key":"S0956796816000307_ref17","unstructured":"McBride C. (2011) Ornamental Algebras, Algebraic Ornaments. Unpublished manuscript."},{"key":"S0956796816000307_ref19","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"S0956796816000307_ref5","doi-asserted-by":"crossref","unstructured":"Cockx J. , Devriese D. & Piessens F. (2014) Pattern matching without K. In International Conference on Functional Programming, Manuel M.T. Chakravarty (ed), ICFP'14. New York, NY, USA: ACM, pp. 257\u2013268.","DOI":"10.1145\/2628136.2628139"},{"key":"S0956796816000307_ref15","first-page":"86","volume-title":"Logic in Computer Science","author":"Kopylov","year":"2003"},{"key":"S0956796816000307_ref14","first-page":"37","volume-title":"Dependently Typed Programming","author":"Ko","year":"2013"},{"key":"S0956796816000307_ref24","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1145\/2633628.2633631","volume-title":"Workshop on Generic Programming","author":"Williams","year":"2014"},{"key":"S0956796816000307_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"S0956796816000307_ref7","volume-title":"Elaborating Inductive Definitions","author":"Dagand","year":"2013"},{"key":"S0956796816000307_ref16","volume-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"S0956796816000307_ref22","volume-title":"Purely Functional Data Structures","author":"Okasaki","year":"1999"},{"key":"S0956796816000307_ref20","unstructured":"Norell U. (2007) Towards a Practical Programming Language Based on Dependent Type Theory. PhD Thesis, Chalmers University of Technology."},{"key":"S0956796816000307_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000069"},{"key":"S0956796816000307_ref12","unstructured":"Ko H.-S. (2014) Analysis and Synthesis of Inductive Families. DPhil Thesis, University of Oxford."},{"key":"S0956796816000307_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863547"},{"key":"S0956796816000307_ref9","unstructured":"Devriese D. & Piessens F. (2011) On the bright side of type classes: Instance arguments in Agda. In Proceedings of International Conference on Functional Programming, Olivier Danvy (ed), ICFP'11. New York, NY, USA: ACM, pp. 143\u2013155."},{"key":"S0956796816000307_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/11780274_27"},{"key":"S0956796816000307_ref13","doi-asserted-by":"publisher","DOI":"10.2201\/NiiPi.2013.10.5"},{"key":"S0956796816000307_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24849-1_8"},{"key":"S0956796816000307_ref6","doi-asserted-by":"crossref","unstructured":"Czarnecki K. , Foster J. N. , Hu Z. , L\u00e4mmel R. , Sch\u00fcrr A. & Terwilliger J. F. (2009) Bidirectional transformations: A cross-discipline perspective. In Proceedings of International Conference on Model Transformation, Richard F. Paige (ed), Lecture Notes in Computer Science, vol. 5563. Berlin, Germany: Springer-Verlag, pp. 260\u2013283.","DOI":"10.1007\/978-3-642-02408-5_19"},{"key":"S0956796816000307_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04652-0_5"},{"key":"S0956796816000307_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03153-3_2"},{"key":"S0956796816000307_ref23","first-page":"158","volume-title":"Central European Functional Programming School","author":"Sheard","year":"2007"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796816000307","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:19:48Z","timestamp":1776889188000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796816000307\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"references-count":24,"alternative-id":["S0956796816000307"],"URL":"https:\/\/doi.org\/10.1017\/s0956796816000307","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"article-number":"e2"}}