Deriving generic class instances for datatypes

 

Title: Deriving generic class instances for datatypes
Authors: Jonas Rädle (jonas /dot/ raedle /at/ tum /dot/ de) and Lars Hupel
Submission date: 2018-11-06
Abstract:

We provide a framework for automatically deriving instances for generic type classes. Our approach is inspired by Haskell's generic-deriving package and Scala's shapeless library. In addition to generating the code for type class functions, we also attempt to automatically prove type class laws for these instances. As of now, however, some manual proofs are still required for recursive datatypes.

Note: There are already articles in the AFP that provide automatic instantiation for a number of classes. Concretely, Deriving allows the automatic instantiation of comparators, linear orders, equality, and hashing. Show instantiates a Haskell-style show class.

Our approach works for arbitrary classes (with some Isabelle/HOL overhead for each class), but a smaller set of datatypes.

BibTeX:
@article{Generic_Deriving-AFP,
  author  = {Jonas Rädle and Lars Hupel},
  title   = {Deriving generic class instances for datatypes},
  journal = {Archive of Formal Proofs},
  month   = nov,
  year    = 2018,
  note    = {\url{http://isa-afp.org/entries/Generic_Deriving.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License