An Effective Proof Rule for General Type Classes

Type classes are a widely adopted means of abstraction for overloading in functional programming languages. Although operating on different types, in general all instances of a class implement equivalent operations and hence have properties in common. Using formal reasoning, such a property can be proven by showing it holds for all instance definitions. This is not straightforward, however, because when instance definitions depend on each other, so will the proofs. The proof assistant ISABELLE supports single parameter type classes and a proof rule for it based on structural induction on types. This method suffices for simple single parameter type classes, but does not lead to a user friendly tactic for more complex forms of overloading. In this paper, an effective proof rule is presented that works for all common extensions to type classes by using an induction scheme derived from the instance definitions. Moreover, it can be easily transformed into a user friendly tactic. This tactic will be implemented in the proof assistant SPARKLE.