Categorical organisation of the ornament–refinement framework

Abstract

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 ornaments to a framework of ornaments and refinements to support a modular structure for dependently typed libraries. We use lightweight category theory to organise the ornament–refinement framework and establish that parallel composition 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.

Supplementary material

The Agda code for the ornament–refinement framework can be found on GitHub, along with other ornament-related constructions developed for the first author’s thesis.

The result was reported in the 2014 Dependently Typed Programming workshop. The slides can be downloaded here.