Deriving class instances for datatypes

 

Title: Deriving class instances for datatypes
Authors: Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
Submission date: 2015-03-11
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.

BibTeX:
@article{Deriving-AFP,
  author  = {Christian Sternagel and René Thiemann},
  title   = {Deriving class instances for datatypes},
  journal = {Archive of Formal Proofs},
  month   = mar,
  year    = 2015,
  note    = {\url{http://isa-afp.org/entries/Deriving.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Collections
Used by: Algebraic_Numbers, CAVA_Automata, Containers, Datatype_Order_Generator, Formula_Derivatives, LTL_to_GBA, MSO_Regex_Equivalence, Promela, Show