### 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.

### License

BSD License

### Topics

- Computer science/Data structures

### Session Generic_Deriving

- Tagged_Prod_Sum
- Derive
- Derive_Datatypes
- Derive_Eq
- Derive_Encode
- Derive_Algebra
- Derive_Show
- Derive_Eq_Laws
- Derive_Algebra_Laws

## Cite

×

Generic_Deriving-AFP

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

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Nov 21, 2018 : Isabelle2018