CHAPTER 1
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 the instance definitions to solve this problem. Using this induction scheme, a proof rule and tactic are defined that are both strong enough and effective.
As a proof of concept, we have implemented the tactic in the proof assistant SPARKLE for the programming language CLEAN. The results, however, are generally applicable and can, for example, also be used for Haskell and Isabelle, if Isabelle would support the specification of general type classes. In fact, the examples here are presented using Haskell syntax. Sparkle is dedicated to Clean, but can also be used to prove properties about Haskell programs by translating them to Clean using the Hacle translator [Nay04].
1.1.3 Outline
The rest of this paper is structured as follows. First, the proof assistant Sparkle is presented (Section 1.2). Then, basic definitions for instance definitions, evidence values, and class constrained properties are introduced (Section 1.3). After showing why structural induction does not suffice (Section 1.4), the proof rule and tactic based on the instance definitions are defined (Section 1.5) and extended to multiple class constraints (Section 1.6). We end with a discussion of the implementation (Section 1.7), related and future work (Section 1.8), and a summary of the results (Section 1.9).
1.2 SPARKLE
The need for this work arose whilst improving the proof support for type classes in Sparkle. Sparkle is a proof assistant specifically geared towards Clean, which means that it can reason about Clean concepts using rules based on Clean's semantics. Properties are specified in a first order predicate logic extended with equality on expressions. An example of this, using a slightly simplified syntax, is:
example:? [for all] n: Int|n≠[perpendicular to] [for all]a [for all] xs: [a] [for all] take n xs ++ drop n xs = xs]
These properties can be proven using tactics, which are user friendly operations that transform a property into a number of logically stronger properties, the proof obligations or goals, that are easier to prove. A tactic is the implementation of (a combination of) theoretically sound proof rules. Whereas in general a proof rule is theoretically simple but not very prover friendly, a tactic is prover friendly but often theoretically more complex. The proof is complete when all remaining proof obligations are trivial. Some useful tactics are, for example, reduction of expressions, induction on expression variables, and rewriting using hypotheses.
In Sparkle, properties that contain member functions can only be proven for specific instances of that function. For example:
sym[Int]:[for all]x:[Int][for all]y:[Int] [x == y -> y == x]
can be easily proven by induction on lists using symmetry of equality on integers. Proving that something holds for all instances, however, is not possible in general. Consider for example symmetry of equality:
sym: [for all]a[Eq :: a [??][for all]x:a [for all]y:x[x == y -> y == x]]
where Eq :: a denotes the, previously not available, constraint that equality must be defined for type a. This property can be split into a property for every instance definition, which gives among others the property for the instance for lists:
sym[a]: [for all]a[Eq :: a [??][for all]x:[a] [for all]y:[a] [x = = y right arrow] y == x]]
It is clear that this property is true as long as it is true for instance a. Unfortunately, this hypothesis is not available. Using an approach based on induction, however, we may be able to assume the hypotheses for all instances the instance definition depends on, and hence will be able to prove the property.
Internally, Sparkle translates type classes to evidence values or dictionaries [WB89], that make the use of overloading explicit. The evidence value for a class constraint c :: a is the evidence that there is an (implementation of the) instanceof class c for type a. Hence, an evidence value exists if and only if the class constraint is satisfied. As usual, we will use the implementation itself as the evidence value. A program is translated by converting all instance definitions to functions (distinct names are created by suffixes). In expressions, the evidence value is substituted for member applications. When functions require certain classes to be defined, the evidence values for these constraints are passed as a parameter. Figure 1.3 shows an example of the result of the translation of the equality class from Figure 1.1.
1.3 PRELIMINARIES
Instead of defining a proof rule that operates on the example properties from Section 1.2, we define both instances and properties at the level that explicitly uses evidence values. In this section, basic definitions for instance definitions, evidence values, and class constrained properties are given.
1.3.1 Instance definitions
Because we intend to support constructor classes, types are formalized by a language of constructors [Jon93]:
τ ::= α| X | τ τ'
where α and x range over a given set of type variables and type constructors respectively. For example, τ can be Int, [Int], and Tree Char, but also the [], Tree, and -> constructors that take types as an argument and yield a list, tree, or function type respectively. TV (τ) denotes the set of type variables occurring in τ. The set of closed types TMc is the set of types for which TV (τ) is empty.
Predicates are used to indicate that an instance of a certain class exists. An instance can be identified by an instantiation of the class parameters. The predicate c :: τ denotes that there is an instance of the class c for instantiation τ of the class parameters. For example, Eq :: [Int] and Eq :: (Int, Int) denote that there is an instance of the Eq class for types [Int] and (Int, Int) respectively:
π ::= c :: τ
Because these predicates are used to constrain types to a certain class, they are called class constraints. Class constraints in which only type variables occur in the type, for example Eq :: a, are called simple. For reasons of simplicity, it is assumed that all type variables that occur in a class constraint are distinct.
Without loss of generality, throughout this paper we restrict ourselves to type classes that have only one member and no subclasses. Multiple members and subclasses can be supported using records of expressions for the evidence values. An instance definition:
inst π [??] c :: τ = e
defines an instance [bar.τ] of class c for types that satisfy class constraints [bar.π]. The instance definition provides the translated expression e for the class member c. The functions Head (inst c :: [bar.π] [??] τ = e) = τ and Context (inst c :: [bar.π] [??]τ = e) = [bar.π] will be used to retrieve the instance head and context respectively.
The program context Ψ that contains the function and class definitions, also includes the available instance definitions. The function IdefsΨ(c) returns the set of instance definitions of class c defined in program Ψ.
1.3.2 Evidence values
From the translation from type classes to evidence values, as briefly summarized in Section 1.2, the rule for evidence creation is important for our purpose. Two definitions are required before it can be defined.
Firstly, because instance definitions are allowed to overlap, a mechanism is needed that chooses between them. Since the exact definition is not important for our purpose, we assume that the function AiΨ (c :: [bar.τ]) determines the most specific instance definition applicable for instance τ of class c. AiΨ is also defined for types that contain variables as long as it can be determined which instance definition should be applied.
Secondly, the dependencies of an instance are the instances it depends on:
Deps (c :: [bar.τ], i) = *Head([i] -> [bar.τ])(Context(i))
where [MATHEMATICAL EXPRESSION OMITTED] denotes the substitutor that maps the type variables in [bar.τ] such that [MATHEMATICAL EXPRESSION OMITTED]. When i is not provided, AiΨ(c :: τ) is assumed for it.
Evidence values are now straightforwardly created by applying the expression of the most specific instance definition to the evidence values of its dependencies:
[MATHEMATICAL EXPRESSION OMITTED]
In proofs, evidence values will be created assuming the evidence values for the dependencies are already assigned to expression variables:
[MATHEMATICAL EXPRESSION OMITTED]
assuming that the evidence for π is assigned to the variable evπ. A specific instance definition i can be provided, because AiΨ might not be known in proofs.
1.3.3 Class constrained properties
In Sparkle, properties are formalized by a first order predicate logic extended with equality on expressions. The equality on expressions is designed to handle infinite and undefined expressions well.
We extend these properties with class constraints, that can be used to constrain types to a certain class. These properties will be referred to as class constrained properties. For example, consider symmetry and transitivity of equality:
sym: [MATHEMATICAL EXPRESSION OMITTED]
trans: [MATHEMATICAL EXPRESSION OMITTED]
The property c :: [bar.τ] [??] p means that in property p it is assumed that [bar.τ] is an instance of class c and the evidence value for this class constraint is assigned to ev[c::]τ. Thus, the semantics of the property π [??] p is defined as [MATHEMATICAL EXPRESSION OMITTED].
1.4 STRUCTURAL INDUCTION
The approach for proving properties that contain overloaded identifiers taken in Isabelle essentially is structural induction on types. In this section it is argued that the proof rule for general type classes should use another induction scheme.
Structural induction on types seems an effective approach because it gives more information about the type of an evidence value. This information can be used to expand evidence values. For example, evEq::[a] can be expanded to eqlist evEq::a (see Figure 1.3).
[MATHEMATICAL EXPRESSION OMITTED]
More importantly, structural induction allows the property to be assumed for structurally smaller types. Ideally the hypothesis should be assumed for all dependencies on the same class. Unfortunately, structural induction does not always allow this for multi parameter classes.
Consider for example the multi parameter class in Figure 1.2. The instance of Eq2 for [Int] (Char, Char) depends on the instance for Char Int, which is not structurally smaller because Char is not structurally smaller than [Int], and Int is not structurally smaller than (Char, Char). Hence, the hypothesis cannot be assumed for this dependency. This problem can be solved by basing the induction scheme on the instance definitions.
1.5 INDUCTION ON INSTANCES
The induction scheme proposed in the previous section can be used on the set of defined instances of a class. In this section, a proof rule and tactic that use this scheme are defined and applied to some examples.
1.5.1 Proof rule and tactic
We first define the set of instances of a class and an order based on the instance definitions on it. The well-founded induction theorem applied to the defined set and order yields the proof rule. Then, the tactic is presented that can be derived from this rule.
