Generic datatypes à la carte [pdf] [bib]

Abstract

Formal reasoning in proof assistants, also known as mechanization, has high development costs. Building modular reusable components is a key issue in reducing these costs. A stumbling block for reuse is that inductive definitions and proofs are closed to extension. This is a manifestation of the expression problem that has been addressed by the Meta-Theory à la Carte (MTC) framework in the context of programming language meta-theory. However, MTC’s use of extensible Church-encodings is unsatisfactory.

This paper takes a better approach to the problem with datatype-generic programming (DGP). It applies well-known DGP techniques to represent modular datatypes, to build functions from functor algebras with folds and to compose proofs from proof algebras by means of induction. Moreover, for certain functionality and proofs our approach can achieve more reuse than MTC: instead of composing modular components we provide a single generic definition once and for all.

BibTeX

@inproceedings{gdtc,
  author =    "Keuchel, Steven and Schrijvers, Tom",
  title =     "Generic Datatypes à la Carte",
  booktitle = "Proceedings of the 9th ACM SIGPLAN workshop on 
               Generic programming",
  series =    "WGP '13",
  year =      "2013",
  isbn =      "978-1-4503-2389-5",
  numpages =  "11",
  doi =       "10.1145/2502488.2502491",
  publisher = "ACM",
  note =      "Boston, Massachusetts, USA, September 28, 2013"
}

Submission Annex

The developments of this paper can be found in this GitHub repository.