Type Classes¶
This chapter presents a quick reference of the commands related to type classes. For an actual introduction to typeclasses, there is a description of the system [SO08] and the literature on type classes in Haskell which also applies.
Class and Instance declarations¶
The syntax for class and instance declarations is the same as the record syntax of Coq:
Class Id (
p\(_{1}\) :
t\(_{1}\) ) ⋯ (
p\(_{n}\) :
t\(_{n}\) ) [:
sort] := {
f\(_{1}\) :
u\(_{1}\) ; ⋮
f\(_{m}\) :
u\(_{m}\) }.
Instance ident : Id
p\(_{1}\) ⋯
p\(_{n}\) := {
f\(_{1}\) :=
t\(_{1}\) ; ⋮
f\(_{m}\) :=
t\(_{m}\) }.
The p\(_{i}\) :
t\(_{i}\) variables are called the parameters of the class and
the f\(_{i}\) :
t\(_{i}\) 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:
- Class EqDec (A : Type) := { eqb : A -> A -> bool ; eqb_leibniz : forall x y, eqb x y = true -> x = y }.
- EqDec is defined eqb is defined eqb_leibniz is defined
This class implements a boolean equality test which is compatible with Leibniz equality on some type. An example implementation is:
- Instance unit_EqDec : EqDec unit := { eqb x y := true ; eqb_leibniz x y H := match x, y return x = y with tt, tt => eq_refl tt end }.
- unit_EqDec is defined
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.:
- Instance eq_bool : EqDec bool := { eqb x y := if x then y else negb y }.
- 1 subgoal ============================ forall x y : bool, (if x then y else negb y) = true -> x = y
- Proof.
- intros x y H.
- 1 subgoal x, y : bool H : (if x then y else negb y) = true ============================ x = y
- destruct x ; destruct y ; (discriminate || reflexivity).
- No more subgoals.
- Defined.
- 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.
Binding classes¶
Once a typeclass is declared, one can use it in class binders:
- 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:
- Fail Definition neqb' (A : Type) (x y : A) := negb (eqb x y).
- The command has indeed failed with message: Unable to satisfy the following constraints: In environment: A : Type x, y : A ?EqDec : "EqDec 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:
- 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 typeclasses:
- They automatically set the maximally implicit status for typeclass
arguments, making derived functions as easy to use as class methods.
In the example above,
A
andeqa
should be set maximally implicit. - They support implicit quantification on partially applied type classes (Implicit generalization). Any argument not given as part of a typeclass binder will be automatically generalized.
- They also support implicit quantification on Superclasses.
Following the previous example, one can write:
- Generalizable Variables A B C.
- Definition neqb_implicit `{eqa : EqDec A} (x y : A) := negb (eqb x y).
- neqb_implicit is defined
Here A
is implicitly generalized, and the resulting function is
equivalent to the one above.
Parameterized Instances¶
One can declare parameterized instances as in Haskell simply by giving the constraints as a binding context before the instance, e.g.:
- Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) := { eqb x y := match x, y with | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb) 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
- Abort.
These instances are used just as well as lemmas in the instance hint database.
Sections and contexts¶
To ease the parametrization of developments by typeclasses, 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, except it accepts any binding context as argument. For example:
- Section EqDec_defs.
- Context `{EA : EqDec A}.
- A is declared EA is declared
- Global Instance option_eqb : EqDec (option A) := { eqb x y := match x, y with | Some x, Some y => eqb x y | None, None => true | _, _ => false end }.
- 1 subgoal A : Type EA : EqDec A ============================ forall x y : option A, match x with | Some x0 => match y with | Some y0 => eqb x0 y0 | None => false end | None => match y with | Some _ => false | None => true end end = true -> x = y
- Admitted.
- option_eqb is declared
- End EqDec_defs.
- 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 _] 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.
Building hierarchies¶
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:
- Class Ord `(E : EqDec A) := { le : A -> A -> bool }.
- Ord is defined le is defined
Contrary to Haskell, we have no special syntax for superclasses, but this declaration is 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.
- Definition le_eqb `{Ord A} (x y : A) := andb (le x y) (le y x).
- le_eqb is defined
In some cases, to be able to specify sharing of structures, one may
want to give explicitly the superclasses. It is is possible to do it
directly in regular binders, and using the !
modifier in class
binders. For example:
- Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := andb (le x y) (neqb x y).
- lt is defined
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.
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.:
- Require Import Relation_Definitions.
- Class Reflexive (A : Type) (R : relation A) := reflexivity : forall x, R x x.
- Class Transitive (A : Type) (R : relation A) := transitivity : forall x y z, R x y -> R y z -> R x z.
This declares singleton classes for reflexive and transitive relations, (see the singleton class variant for an explanation). These may be used as parts of other classes:
- Class PreOrder (A : Type) (R : relation A) := { PreOrder_Reflexive :> Reflexive A R ; PreOrder_Transitive :> Transitive A R }.
- PreOrder is defined PreOrder_Reflexive is defined PreOrder_Transitive is defined
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.
Summary of the commands¶
-
Command
Class ident binders? : sort? := ident? { ident :>? term+; }
¶ The
Class
command is used to declare a typeclass with parametersbinders
and fields the declared record fields.
Variants:
-
Command
Class ident binders? : sort? := ident : term
This variant declares a singleton class with a single method. This singleton class is a so-called definitional class, represented simply as a definition
ident binders := term
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.
-
Command
Existing Class ident
¶ This variant declares a class a posteriori from a constant or inductive definition. No methods or instances are defined.
The Instance
command is used to declare a typeclass instance named
ident
of the class Class
with parameters t1
to tn
and
fields b1
to bi
, where each field must be a declared field of
the class. Missing fields must be filled in interactive proof mode.
An arbitrary context of binders
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. If the priority is not specified, it defaults to the number
of non-dependent binders of the instance.
-
Variant
Instance ident binders? : forall binders?, Class t1 … tn [| priority] := term
This syntax is used for declaration of singleton class instances or for directly giving an explicit term of type
forall binders, Class t1 … tn
. One need not even mention the unique field name for singleton classes.
-
Variant
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.
-
Variant
Program Instance
¶ Switches the type checking to Program (chapter Program) and uses the obligation mechanism to manage missing fields.
-
Variant
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 betweenDeclare Module
andModule
.
Besides the Class
and Instance
vernacular commands, there are a
few other commands related to typeclasses.
-
Command
Existing Instance ident+ [| priority]
¶ This command adds an arbitrary list of constants whose type ends with an applied typeclass to the instance database with an optional priority. It can be used for redeclaring instances at the end of sections, or declaring structure projections as instances. This is equivalent to
Hint Resolve ident : typeclass_instances
, except it registers instances forPrint Instances
.
-
Command
Context binders
¶ Declares variables according to the given binding context, which might use Implicit generalization.
-
typeclasses eauto
¶ This tactic uses a different resolution engine than
eauto
andauto
. The main differences are the following:Contrary to
eauto
andauto
, the resolution is done entirely in the new proof engine (as of Coq 8.6), meaning that backtracking is available among dependent subgoals, and shelving goals is supported.typeclasses eauto
is a multi-goal tactic. It analyses the dependencies between subgoals to avoid backtracking on subgoals that are entirely independent.When called with no arguments,
typeclasses eauto
uses thetypeclass_instances
database by default (instead of core). Dependent subgoals are automatically shelved, and shelved goals can remain after resolution ends (following the behavior of Coq 8.5).Note
As of Coq 8.6,
all:once (typeclasses eauto)
faithfully mimicks what happens during typeclass resolution when it is called during refinement/type inference, except that only declared class subgoals are considered at the start of resolution during type inference, whileall
can select non-class subgoals as well. It might move toall:typeclasses eauto
in future versions when the refinement engine will be able to backtrack.When called with specific databases (e.g. with),
typeclasses eauto
allows shelved goals to remain at any point during search and treat typeclass goals like any other.The transparency information of databases is used consistently for all hints declared in them. It is always used when calling the unifier. When considering local hypotheses, we use the transparent state of the first hint database given. Using an empty database (created with
Create HintDb
for example) with unfoldable variables and constants as the first argument oftypeclasses eauto
hence makes resolution with the local hypotheses use full conversion during unification.
-
Variant
typeclasses eauto num
-
Variant
typeclasses eauto with ident+
This variant runs resolution with the given hint databases. It treats typeclass subgoals the same as other subgoals (no shelving of non-typeclass goals in particular).
-
autoapply term with ident
¶ The tactic
autoapply
applies a term using the transparency information of the hint database ident, and does no typeclass resolution. This can be used inHint Extern
’s for typeclass instances (in the hint databasetypeclass_instances
) to allow backtracking on the typeclass subgoals created by the lemma application, rather than doing typeclass resolution locally at the hint application time.
Typeclasses Transparent, Typclasses Opaque¶
-
Command
Typeclasses Transparent ident+
¶ This command makes the identifiers transparent during typeclass resolution.
-
Command
Typeclasses Opaque ident+
¶ Make the identifiers opaque for typeclass search. 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 The hints databases for auto and eauto).
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
.
Options¶
-
Flag
Typeclasses Dependency Order
¶ This option (on by default since 8.6) respects the dependency order between subgoals, meaning that subgoals on which other subgoals depend come first, while the non-dependent subgoals were put before the dependent ones previously (Coq 8.5 and below). This can result in quite different performance behaviors of proof search.
-
Flag
Typeclasses Filtered Unification
¶ This option, available since Coq 8.6 and off by default, switches the hint application procedure to a filter-then-unify strategy. To apply a hint, we first check that the goal matches syntactically the inferred or specified pattern of the hint, and only then try to unify the goal with the conclusion of the hint. This can drastically improve performance by calling unification less often, matching syntactic patterns being very quick. This also provides more control on the triggering of instances. For example, forcing a constant to explicitely appear in the pattern will make it never apply on a goal where there is a hole in that place.
-
Flag
Typeclasses Limit Intros
¶ This option (on by default) controls the ability to apply hints while avoiding (functional) eta-expansions in the generated proof term. It does so by allowing hints that conclude in a product to apply to a goal with a matching product directly, avoiding an introduction.
Warning
This can be expensive as it requires rebuilding hint clauses dynamically, and does not benefit from the invertibility status of the product introduction rule, resulting in potentially more expensive proof-search (i.e. more useless backtracking).
-
Flag
Typeclass Resolution For Conversion
¶ This option (on by default) controls the use of typeclass resolution when a unification problem cannot be solved during elaboration/type inference. With this option on, when a unification fails, typeclass resolution is tried before launching unification once again.
-
Flag
Typeclasses Strict Resolution
¶ Typeclass declarations introduced when this option is set have a stricter resolution behavior (the option is off by default). When looking for unifications of a goal with an instance of this class, we “freeze” all the existentials appearing in the goals, meaning that they are considered rigid during unification and cannot be instantiated.
-
Flag
Typeclasses Unique Solutions
¶ When a typeclass resolution is launched we ensure that it has a single solution or fail. This ensures that the resolution is canonical, but can make proof search much more expensive.
-
Flag
Typeclasses Unique Instances
¶ Typeclass declarations introduced when this option is set have a more efficient resolution behavior (the option is off by default). When a solution to the typeclass goal of this class is found, we never backtrack on it, assuming that it is canonical.
-
Flag
Typeclasses Debug
¶ Controls whether typeclass resolution steps are shown during search. Setting this flag also sets
Typeclasses Debug Verbosity
to 1.
-
Option
Typeclasses Debug Verbosity num
¶ Determines how much information is shown for typeclass resolution steps during search. 1 is the default level. 2 shows additional information such as tried tactics and shelving of goals. Setting this option also sets
Typeclasses Debug
.
-
Flag
Refine Instance Mode
¶ This option allows to switch the behavior of instance declarations made through the Instance command.
- When it is on (the default), instances that have unsolved holes in their proof-term silently open the proof mode with the remaining obligations to prove.
- When it is off, they fail with an error instead.
Typeclasses eauto :=¶
-
Command
Typeclasses eauto := debug? {dfs | bfs}? depth
¶ This command allows more global customization of the typeclass resolution tactic. The semantics of the options 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 limit of the search.