Categorical organisation of the ornament–refinement framework
<p>Dependently typed programming uses precise variants of data structures to ensure program correctness in an economical way, but designing reusable libraries for all possible variants of data structures is a difficult problem. The authors addressed the problem by extending McBride’s <em>...
| Main Authors: | , |
|---|---|
| Format: | Record |
| Published: |
Submitted to POPL'14
2013
|
| _version_ | 1826285076219953152 |
|---|---|
| author | Ko, H Gibbons, J |
| author_facet | Ko, H Gibbons, J |
| author_sort | Ko, H |
| collection | OXFORD |
| description | <p>Dependently typed programming uses precise variants of data structures to ensure program correctness in an economical way, but designing reusable libraries for all possible variants of data structures is a difficult problem. The authors addressed the problem by extending McBride’s <em>ornaments</em> to a framework of ornaments and <em>refinements</em> to support a modular structure for dependently typed libraries. We use lightweight category theory to organise the ornament–refinement framework and establish that <em>parallel composition</em> of ornaments, a key construction in the framework, gives rise to certain pullback properties. Two important sets of isomorphisms in the framework are then reconstructed using the pullback properties. This categorical organisation — which is completely formalised in the dependently typed language Agda — helps to separate the lower-level detail of the universes from the higher-level constructions of the isomorphisms, and to gain an abstract and effective understanding of the isomorphisms and the overall structure of the framework.</p> <h3>Supplementary material</h3> <p>The Agda code for the ornament–refinement framework can be found on <a href="https://github.com/josh-hs-ko/Thesis">GitHub</a>, along with other ornament-related constructions developed for the first author’s thesis.</p> <p>The result was reported in the <a href="http://eb.host.cs.st-andrews.ac.uk/DTP2014/">2014 Dependently Typed Programming workshop</a>. The slides can be downloaded <a href="http://www.cs.ox.ac.uk/people/hsiang-shang.ko/pcOrn-categorical/DTP.pdf">here</a>. </p> |
| first_indexed | 2024-03-07T01:23:26Z |
| format | Record |
| id | oxford-uuid:91225d69-eaf8-436d-afb7-b898eee3c6ef |
| institution | University of Oxford |
| last_indexed | 2024-03-07T01:23:26Z |
| publishDate | 2013 |
| publisher | Submitted to POPL'14 |
| record_format | dspace |
| spelling | oxford-uuid:91225d69-eaf8-436d-afb7-b898eee3c6ef2022-03-26T23:16:36ZCategorical organisation of the ornament–refinement frameworkRecordhttp://purl.org/coar/resource_type/c_1843uuid:91225d69-eaf8-436d-afb7-b898eee3c6efDepartment of Computer ScienceSubmitted to POPL'142013Ko, HGibbons, J<p>Dependently typed programming uses precise variants of data structures to ensure program correctness in an economical way, but designing reusable libraries for all possible variants of data structures is a difficult problem. The authors addressed the problem by extending McBride’s <em>ornaments</em> to a framework of ornaments and <em>refinements</em> to support a modular structure for dependently typed libraries. We use lightweight category theory to organise the ornament–refinement framework and establish that <em>parallel composition</em> of ornaments, a key construction in the framework, gives rise to certain pullback properties. Two important sets of isomorphisms in the framework are then reconstructed using the pullback properties. This categorical organisation — which is completely formalised in the dependently typed language Agda — helps to separate the lower-level detail of the universes from the higher-level constructions of the isomorphisms, and to gain an abstract and effective understanding of the isomorphisms and the overall structure of the framework.</p> <h3>Supplementary material</h3> <p>The Agda code for the ornament–refinement framework can be found on <a href="https://github.com/josh-hs-ko/Thesis">GitHub</a>, along with other ornament-related constructions developed for the first author’s thesis.</p> <p>The result was reported in the <a href="http://eb.host.cs.st-andrews.ac.uk/DTP2014/">2014 Dependently Typed Programming workshop</a>. The slides can be downloaded <a href="http://www.cs.ox.ac.uk/people/hsiang-shang.ko/pcOrn-categorical/DTP.pdf">here</a>. </p> |
| spellingShingle | Ko, H Gibbons, J Categorical organisation of the ornament–refinement framework |
| title | Categorical organisation of the ornament–refinement framework |
| title_full | Categorical organisation of the ornament–refinement framework |
| title_fullStr | Categorical organisation of the ornament–refinement framework |
| title_full_unstemmed | Categorical organisation of the ornament–refinement framework |
| title_short | Categorical organisation of the ornament–refinement framework |
| title_sort | categorical organisation of the ornament refinement framework |
| work_keys_str_mv | AT koh categoricalorganisationoftheornamentrefinementframework AT gibbonsj categoricalorganisationoftheornamentrefinementframework |