University of Oxford Logo University of OxfordDepartment of Computer Science - Home
On Facebook
Facebook
Follow us on twitter
Twitter
Linked in
Linked in
Flickr
Flickr
Google plus
Google plus
Digg
Digg
Pinterest
Pinterest
Stumble Upon
Stumble Upon

Modularising inductive families

Hsiang−Shang Ko and Jeremy Gibbons

Abstract

Dependently typed programmers are encouraged to use inductive families to integrate constraints with data construction. Different constraints are used in different contexts, leading to different versions of datatypes for the same data structure. Modular implementation of common operations for these structurally similar datatypes has been a longstanding problem. We propose a datatype-generic solution based on McBride's datatype ornaments, exploiting an isomorphism whose interpretation borrows ideas from realisability. Relevant properties of the operations are separately proven for each constraint, and after the programmer selects several constraints to impose on a basic datatype and synthesises an inductive family incorporating those constraints, the operations can be routinely upgraded to work with the synthesised inductive family.

There is a revised version of this paper in Progress in Informatics.

Supplementary material

The accompanying Agda code can be found here: a plain Agda file or a syntax-highlighted, browsable HTML version.

Two talks were given at DTP'11 and WGP'11: The DTP'11 version (which was reprised in a Shonan meeting on DTP) is more freestyle and includes a development of ornamental-algebraic ornamentation, while the WGP'11 version has a clearer structure and elaborates more on the background.

A related talk on numerical representations, which was more about Pierre and Conor's coherence property, was given at Fun in the Afternoon in Oxford, February 2012.

Details

Book Title

Workshop on Generic Programming

Pages

13−24

Publisher

ACM

Series

WGP'11

Year

2011

Links

BibTeX

Link (pdf)

DOI (10.1145/2036918.2036921)

Download official version from ACM

Related pages

People

Projects

Activities

Themes