Proof Support for General Type Classes

Ron van Kesteren, Marko van Eekelen, Maarten de Mol

Abstract: We present a proof rule and an effective tactic for proving properties about HASKELL type classes by proving them for the available instance definitions. This is not straightforward, because instance definitions may depend on each other. The proof assistant Isabelle handles this problem for single parameter type classes by structural induction on types. However, this does not suffice for an effective tactic for more complex forms of overloading. We solve this using an induction scheme derived from the instance definitions. The tactic based on this rule is implemented in the proof assistant Sparkle.

1.1 INTRODUCTION

It is often stated that formulating properties about programs increases robustness and safety, especially when formal reasoning is used to prove these properties. Robustness and safety are becoming increasingly important considering the current dependence of society on technology. Research on formal reasoning has spawned many general purpose proof assistants, such as COQ [dt04], ISABELLE [NPW02], and PVS [OSRSC99]. Unfortunately, these general purpose tools are geared towards mathematicians and are hard to use when applied to more practical domains such as actual programming languages.

Because of this, proof assistants have been developed that are geared towards specific programming languages. This allows proofs to be conducted on the source program using specifically designed proof rules. Functional languages are especially suited for formal reasoning because they are referentially transparent. Examples of proof assistants for functional languages are EVT [NFD01] for ERLANG [AV91], SPARKLE [dMvEP01] for CLEAN [vEP01], and ERA [Win99] for HASKELL [Jon03].

1.1.1 Type classes

A feature that is commonly found in functional programming languages is over -loading structured by type classes [WB89]. Type classes essentially are groups of types, the class instances, for which certain operations, the class members, are implemented. These implementations are created from the available instance definitions and may be different for each instance. The type of an instance definition is called the instance head. The equality operator will be used as a running example throughout this paper (Figure 1.1).

In the most basic case, type classes have only one parameter and instance heads are flat, that is, a single constructor applied to a list of type variables. Furthermore, no two instance definitions may overlap.

Several significant extensions have been proposed, such as multiple parameters [JJM97], overlapping instances, and instantiation with constructors [Jon93], that have useful applications such as collections, coercion, isomorphisms and mapping. In this paper, the term general type classes is used for systems of type classes that support these extensions and non-flat instance heads. Figure 1.2 shows a multi parameter class for the symmetric operation eq2.

An important observation regarding type classes is that, in general, the defined instances should be semantically related. For example, all instances of the equality operator usually implement an equivalence relation. These properties can be proven for all instances at once by proving them for the available instance definitions. Unfortunately, this is not straightforward because the instance definitions may depend on each other and hence so will the proofs. For example, equality on lists is only symmetric if equality on the list members is so as well.

1.1.2 Contributions

The only proof assistant with special support for overloading that we know of is ISABELLE [Nip93, Wen97], which essentially supports single parameter type classes and a proof rule for it based on structural induction on types. However, we show that for general type classes, an effective tactic is not easily derived when structural induction is used. We use an induction scheme on types based on...