| Sammanfattning: | <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>
|
|---|