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