Deriving class instances for datatypes

Christian Sternagel 📧 and René Thiemann 🌐

March 11, 2015

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

We provide a framework for registering automatic methods to derive class instances of datatypes, as it is possible using Haskell's “deriving Ord, Show, ...” feature.

We further implemented such automatic methods to derive comparators, linear orders, parametrizable equality functions, and hash-functions which are required in the Isabelle Collection Framework and the Container Framework. Moreover, for the tactic of Blanchette to show that a datatype is countable, we implemented a wrapper so that this tactic becomes accessible in our framework. All of the generators are based on the infrastructure that is provided by the BNF-based datatype package.

Our formalization was performed as part of the IsaFoR/CeTA project. With our new tactics we could remove several tedious proofs for (conditional) linear orders, and conditional equality operators within IsaFoR and the Container Framework.

License

BSD License

Topics

Session Deriving