Programming with ornaments
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 rel...
| Main Authors: | , |
|---|---|
| Format: | Journal article |
| Published: |
Cambridge University Press
2016
|
| _version_ | 1826304144236871680 |
|---|---|
| author | Ko, H Gibbons, J |
| author_facet | Ko, H Gibbons, J |
| author_sort | Ko, H |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T06:13:20Z |
| format | Journal article |
| id | oxford-uuid:f0476871-2b2f-48d6-9cbe-645e186cafd7 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T06:13:20Z |
| publishDate | 2016 |
| publisher | Cambridge University Press |
| record_format | dspace |
| spelling | oxford-uuid:f0476871-2b2f-48d6-9cbe-645e186cafd72022-03-27T11:46:32ZProgramming with ornamentsJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:f0476871-2b2f-48d6-9cbe-645e186cafd7Symplectic Elements at OxfordCambridge University Press2016Ko, HGibbons, JDependently 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. |
| spellingShingle | Ko, H Gibbons, J Programming with ornaments |
| title | Programming with ornaments |
| title_full | Programming with ornaments |
| title_fullStr | Programming with ornaments |
| title_full_unstemmed | Programming with ornaments |
| title_short | Programming with ornaments |
| title_sort | programming with ornaments |
| work_keys_str_mv | AT koh programmingwithornaments AT gibbonsj programmingwithornaments |