Chapter 18 Type Classes

# Coq Reference Manual

# Chapter 18 Type Classes

- 18.1 Class and Instance declarations
- 18.2 Binding classes
- 18.3 Parameterized Instances
- 18.4 Sections and contexts
- 18.5 Building hierarchies
- 18.6 Summary of the commands

Matthieu Sozeau

The status of Type Classes is experimental.

This chapter presents a quick reference of the commands related to type classes. For an actual introduction to type classes, there is a description of the system [127] and the literature on type classes in Haskell which also applies.

## 18.1 Class and Instance declarations

The syntax for class and instance declarations is the same as record syntax of Coq:

`Class` `Id` (α1 : τ1) ⋯ (αn : τn) [: sort] := {
| f1 | : | type1 ;
| ⋮ |  |
| fm | : | typem }.

`Instance` ident : `Id` term1 ⋯ termn := {
| f1 | := | termf1 ;
| ⋮ |  |
| fm | := | termfm }.

The αi : τi variables are called the parameters of the class and the fk : typek are called the methods. Each class definition gives rise to a corresponding record declaration and each instance is a regular definition whose name is given by ident and type is an instantiation of the record type.

We’ll use the following example class in the rest of the chapter:

`Coq` `<``Class EqDec (A : Type) := {`
`Coq` `<``eqb : A -``>``A -``>``bool ;`
`Coq` `<``eqb_leibniz : forall x y, eqb x y = true -``>``x = y }.`

This class implements a boolean equality test which is compatible with Leibniz equality on some type. An example implementation is:

`Coq` `<``Instance unit_EqDec : EqDec unit :=`
`Coq` `<``{ eqb x y := true ;`
`Coq` `<``eqb_leibniz x y H :=`
`Coq` `<``match x, y return x = y with tt, tt =``>``refl_equal tt end }.`

If one does not give all the members in the `Instance` declaration, Coq enters the proof-mode and the user is asked to build inhabitants of the remaining fields, e.g.:

`Coq` `<``Instance eq_bool : EqDec bool :=`
`Coq` `<``{ eqb x y := if x then y else negb y }.`
`Coq` `<``Proof. intros x y H.`
`1 subgoal`
``
`x : bool`
`y : bool`
`H : (if x then y else negb y) = true`
`============================`
`x = y`
`Coq` `<``destruct x ; destruct y ; (discriminate || reflexivity).`
`Proof completed.`
`Coq` `<``Defined.`
`refine {|`
`eqb := fun x y : bool =``>``if x then y else negb y;`
`eqb_leibniz := _`
`:forall x y : bool,`
`(if x then y else negb y) = true -``>``x = y |}.`
`intros x y H.`
`destruct x; destruct y; discriminate || reflexivity.`
`eq_bool is defined`

One has to take care that the transparency of every field is determined by the transparency of the `Instance` proof. One can use alternatively the `Program` `Instance` variant which has richer facilities for dealing with obligations.

## 18.2 Binding classes

Once a type class is declared, one can use it in class binders:

`Coq` `<``Definition neqb {A} {eqa : EqDec A} (x y : A) := negb (eqb x y).`
`neqb is defined`

When one calls a class method, a constraint is generated that is satisfied only in contexts where the appropriate instances can be found. In the example above, a constraint `EqDec A` is generated and satisfied by `eqa : EqDec A`. In case no satisfying constraint can be found, an error is raised:

`Coq` `<``Definition neqb’ (A : Type) (x y : A) := negb (eqb x y).`
`Toplevel input, characters 47-50:`
`>``Definition neqb’ (A : Type) (x y : A) := negb (eqb x y).`
`>``` `^``^``^`
`Error: Cannot infer the implicit parameter EqDec of`
`eqb.`
`Could not find an instance for "EqDec A" in environment:`
`A : Type`
`x : A`
`y : A`

The algorithm used to solve constraints is a variant of the eauto tactic that does proof search with a set of lemmas (the instances). It will use local hypotheses as well as declared lemmas in the `typeclass_instances` database. Hence the example can also be written:

`Coq` `<``Definition neqb’ A (eqa : EqDec A) (x y : A) := negb (eqb x y).`
`neqb’ is defined`

However, the generalizing binders should be used instead as they have particular support for type classes:

- They automatically set the maximally implicit status for type class arguments, making derived functions as easy to use as class methods. In the example above, `A` and `eqa` should be set maximally implicit.
- They support implicit quantification on partialy applied type classes.
- They also support implicit quantification on superclasses (§18.5.1)

Following the previous example, one can write:

`Coq` `<``Definition neqb_impl ‘{eqa : EqDec A} (x y : A) := negb (eqb x y).`
`neqb_impl is defined`

Here `A` is implicitly generalized, and the resulting function is equivalent to the one above.

The parsing of generalized type-class binders is different from regular binders:

- Implicit arguments of the class type are ignored.
- Superclasses arguments are automatically generalized.
- Any remaining arguments not given as part of a type class binder will be automatically generalized. In other words, the rightmost parameters are automatically generalized if not mentionned.

One can switch off this special treatment using the ! mark in front of the class name (see example below).

## 18.3 Parameterized Instances

One can declare parameterized instances as in Haskell simply by giving the constraints as a binding context before the instance, e.g.:

`Coq` `<``Instance prod_eqb ‘(EA : EqDec A, EB : EqDec B) : EqDec (A * B) :=`
`Coq` `<``{ eqb x y := match x, y with`
`Coq` `<``| (la, ra), (lb, rb) =``>``andb (eqb la lb) (eqb ra rb)`
`Coq` `<``end }.`
`1 subgoal`
``
`A : Type`
`EA : EqDec A`
`B : Type`
`EB : EqDec B`
`============================`
`forall x y : A * B,`
`(let (la, ra) := x in let (lb, rb) := y in (eqb la lb && eqb ra rb)%bool) =`
`true -``>``x = y`

These instances are used just as well as lemmas in the instance hint database.

## 18.4 Sections and contexts

To ease the parametrization of developments by type classes, we provide a new way to introduce variables into section contexts, compatible with the implicit argument mechanism. The new command works similarly to the `Variables` vernacular (see 1.3.1), except it accepts any binding context as argument. For example:

`Coq` `<``Section EqDec_defs.`
`Coq` `<``Context ‘{EA : EqDec A}.`
`A is assumed`
`EA is assumed`
`Coq` `<``Global Instance option_eqb : EqDec (option A) :=`
`Coq` `<``{ eqb x y := match x, y with`
`Coq` `<``| Some x, Some y =``>``eqb x y`
`Coq` `<``| None, None =``>``true`
`Coq` `<``| _, _ =``>``false`
`Coq` `<``end }.`
`Coq` `<``End EqDec_defs.`
`Coq` `<``About option_eqb.`
`option_eqb : forall A : Type, EqDec A -``>``EqDec (option A)`
`Arguments A, EA are implicit and maximally inserted`
`Argument scopes are [type_scope _]`
`option_eqb is transparent`
`Expands to: Constant Top.option_eqb`

Here the `Global` modifier redeclares the instance at the end of the section, once it has been generalized by the context variables it uses.

## 18.5 Building hierarchies

### 18.5.1 Superclasses

One can also parameterize classes by other classes, generating a hierarchy of classes and superclasses. In the same way, we give the superclasses as a binding context:

`Coq` `<``Class Ord ‘(E : EqDec A) :=`
`Coq` `<``{ le : A -``>``A -``>``bool }.`

Contrary to Haskell, we have no special syntax for superclasses, but this declaration is morally equivalent to:

    Class `(E : EqDec A) => Ord A :=
      { le : A -> A -> bool }.

This declaration means that any instance of the `Ord` class must have an instance of `EqDec`. The parameters of the subclass contain at least all the parameters of its superclasses in their order of appearance (here `A` is the only one). As we have seen, `Ord` is encoded as a record type with two parameters: a type `A` and an `E` of type `EqDec A`. However, one can still use it as if it had a single parameter inside generalizing binders: the generalization of superclasses will be done automatically.

`Coq` `<``Definition le_eqb ‘{Ord A} (x y : A) := andb (le x y) (le y x).`

In some cases, to be able to specify sharing of structures, one may want to give explicitly the superclasses. It is possible to do it directly in regular generalized binders, and using the `!` modifier in class binders. For example:

`Coq` `<``Definition lt ‘{eqa : EqDec A, ! Ord eqa} (x y : A) :=`
`Coq` `<``andb (le x y) (neqb x y).`

The `!` modifier switches the way a binder is parsed back to the regular interpretation of Coq. In particular, it uses the implicit arguments mechanism if available, as shown in the example.

### 18.5.2 Substructures

Substructures are components of a class which are instances of a class themselves. They often arise when using classes for logical properties, e.g.:

`Coq` `<``Class Reflexive (A : Type) (R : relation A) :=`
`Coq` `<``reflexivity : forall x, R x x.`
`Coq` `<``Class Transitive (A : Type) (R : relation A) :=`
`Coq` `<``transitivity : forall x y z, R x y -``>``R y z -``>``R x z.`

This declares singleton classes for reflexive and transitive relations, (see 1 for an explanation). These may be used as part of other classes:

`Coq` `<``Class PreOrder (A : Type) (R : relation A) :=`
`Coq` `<``{ PreOrder_Reflexive :``>``Reflexive A R ;`
`Coq` `<``PreOrder_Transitive :``>``Transitive A R }.`

The syntax `:>` indicates that each `PreOrder` can be seen as a `Reflexive` relation. So each time a reflexive relation is needed, a preorder can be used instead. This is very similar to the coercion mechanism of `Structure` declarations. The implementation simply declares each projection as an instance.

One can also declare existing objects or structure projections using the `Existing Instance` command to achieve the same effect.

## 18.6 Summary of the commands

### 18.6.1 `Class` ident`` binder`1``…` binder`n``:` sort`:= { field``1``; …; field``k``}.`

The `Class` command is used to declare a type class with parameters binder1 to bindern and fields `field``1` to `field``k`.

Variants:

1. `Class` ident`` binder`1``…`binder`n``:` sort`:=` ident`1``:` type`1``.` This variant declares a singleton class whose only method is ident`1`. This singleton class is a so-called definitional class, represented simply as a definition ident`` binder`1``…`binder`n``:=` type`1` and whose instances are themselves objects of this type. Definitional classes are not wrapped inside records, and the trivial projection of an instance of such a class is convertible to the instance itself. This can be useful to make instances of existing objects easily and to reduce proof size by not inserting useless projections. The class constant itself is declared rigid during resolution so that the class abstraction is maintained.
2. `Existing Class` ident`.` This variant declares a class a posteriori from a constant or inductive definition. No methods or instances are defined.

### 18.6.2 `Instance` ident`` binder`1``…`binder`n``:` `Class``` `t``1``…t``n``[|` `priority``] := { field``1``:= b``1``; …; field``i``:= b``i``}`

The `Instance` command is used to declare a type class instance named ident of the class Class with parameters t1 to tn and fields `b``1` to `b``i`, where each field must be a declared field of the class. Missing fields must be filled in interactive proof mode.

An arbitrary context of the form binder`1``…`binder`n` can be put after the name of the instance and before the colon to declare a parameterized instance. An optional priority can be declared, 0 being the highest priority as for auto hints.

Variants:

1. `Instance` ident`` binder`1``…`binder`n``: forall` binder`n+1``…`binder`m``,` `Class``` `t``1``…t``n``[|` `priority``] :=` term This syntax is used for declaration of singleton class instances or for directly giving an explicit term of type `forall` binder`n+1``…`binder`m``,` `Class``` `t``1``…t``n`. One need not even mention the unique field name for singleton classes.
2. `Global Instance` One can use the `Global` modifier on instances declared in a section so that their generalization is automatically redeclared after the section is closed.
3. `Program Instance` Switches the type-checking to Program (chapter 22) and uses the obligation mechanism to manage missing fields.
4. `Declare Instance` In a `Module Type`, this command states that a corresponding concrete instance should exist in any implementation of this `Module Type`. This is similar to the distinction between `Parameter` vs. `Definition`, or between `Declare Module` and `Module`.

Besides the `Class` and `Instance` vernacular commands, there are a few other commands related to type classes.

### 18.6.3 `Existing Instance` ident

This commands adds an arbitrary constant whose type ends with an applied type class to the instance database. It can be used for redeclaring instances at the end of sections, or declaring structure projections as instances. This is almost equivalent to `Hint Resolve` ident`: typeclass_instances`.

### 18.6.4 `Context` binder`1``…`binder`n`

Declares variables according to the given binding context, which might use implicit generalization (see 18.4).

### 18.6.5 `Typeclasses Transparent, Opaque` ident`1``…`ident`n`

This commands defines the transparency of ident1 …identn during type class resolution. It is useful when some constants prevent some unifications and make resolution fail. It is also useful to declare constants which should never be unfolded during proof-search, like fixpoints or anything which does not look like an abbreviation. This can additionally speed up proof search as the typeclass map can be indexed by such rigid constants (see 8.13.1). By default, all constants and local variables are considered transparent. One should take care not to make opaque any constant that is used to abbreviate a type, like `relation A := A -> A -> Prop`.

This is equivalent to `Hint Transparent,Opaque` ident `: typeclass_instances`.

### 18.6.6 `Typeclasses eauto := [debug] [dfs | bfs] [``depth``]`

This commands allows to customize the type class resolution tactic, based on a variant of eauto. The flags semantics are:

- `debug` In debug mode, the trace of successfully applied tactics is printed.
- `dfs, bfs` This sets the search strategy to depth-first search (the default) or breadth-first search.
- depth This sets the depth of the search (the default is 100).