# TypeclassesA Tutorial on Typeclasses in Coq

In real-world programming, it is often necessary to convert
various kinds of data structures into strings so that they can be
printed out, written to files, marshalled for sending over the
network, or whatever. This can be accomplished by writing string
converters for each basic type
plus combinators for structured types like list and pairs
that take string converters for their element types as arguments.
Once we've done this, we can build string converters for more
complex structured types by assembling them from these pieces:
While this idiom gets the job done, it feels a bit clunky in
at least two ways. First, it demands that we give names to all
these string converters (which must later be remembered!) whereas
it seems the names could really just be generated in a uniform way
from the types involved. Moreover, the definitions of converters
like showListOfPairsOfNats are always derived in a quite
mechanical way from their types, together with a small collection
of primitive converters and converter combinators.
The designers of Haskell addressed this clunkiness through
Many other modern language designs have followed Haskell's lead,
and Coq is no exception. However, because Coq's type system is so
much richer than that of Haskell, and because typeclasses in Coq
are used to automatically construct not only programs but also
proofs, Coq's presentation of typeclasses is quite a bit less
"transparent": to use typeclasses effectively, one must have a
fairly detailed understanding of how they are implemented. Coq
typeclasses are a power tool: they can make complex developments
much more elegant and easy to manage when used properly, and they
can cause a great deal of trouble when things go wrong!
This tutorial introduces the core features of Coq's typeclasses,
explains how they are implemented, surveys some useful typeclasses
that can be found in Coq's standard library and other contributed
libraries, and collects some advice about the pragmatics of using
typeclasses.

- showBool : bool → string
- showNat : nat → string
- etc.

- showList : {A : Type} (A → string) → (list A) → string
- showPair : {A B : Type} (A → string) → (B → string) → A × B → string

- showListOfPairsOfNats = showList (showPair showNat showNat)

*typeclasses*, a mechanism by which the typechecker is instructed to automatically construct "type-driven" functions [Wadler and Blott 1989]. (Readers not already familiar with typeclasses should note that, although the word sounds a bit like "classes" from object-oriented programming, this apparent connection is rather misleading. A better analogy is actually with*interfaces*from languages like Java. But best of all is to set aside object-oriented preconceptions and try to approach typeclasses with an empty mind!)# Basics

## Classes and Instances

The Show typeclass can be thought of as "classifying" types
whose values can be converted to strings -- that is, types A
such that we can define a function show of type A → string.
We can declare that bool is such a type by giving an Instance
declaration that witnesses this function:

Here, the export pragma instructs Coq to export this instance
whenever this module is loaded. Other options are local (which
never exports the instance), and global (which always does).

Other types can similarly be equipped with Show instances --
including, of course, new types that we define.

Inductive primary := Red | Green | Blue.

#[export] Instance showPrimary : Show primary :=

{

show :=

fun c:primary ⇒

match c with

| Red ⇒ "Red"

| Green ⇒ "Green"

| Blue ⇒ "Blue"

end

}.

Compute (show Green).

#[export] Instance showPrimary : Show primary :=

{

show :=

fun c:primary ⇒

match c with

| Red ⇒ "Red"

| Green ⇒ "Green"

| Blue ⇒ "Blue"

end

}.

Compute (show Green).

The show function is sometimes said to be
Converting natural numbers to strings is conceptually similar,
though it requires a tiny bit of programming:

*overloaded*, since it can be applied to arguments of many types, with potentially radically different behavior depending on the type of its argument.
Fixpoint string_of_nat_aux (time n : nat) (acc : string) : string :=

let d := match n mod 10 with

| 0 ⇒ "0" | 1 ⇒ "1" | 2 ⇒ "2" | 3 ⇒ "3" | 4 ⇒ "4" | 5 ⇒ "5"

| 6 ⇒ "6" | 7 ⇒ "7" | 8 ⇒ "8" | _ ⇒ "9"

end in

let acc' := d ++ acc in

match time with

| 0 ⇒ acc'

| S time' ⇒

match n / 10 with

| 0 ⇒ acc'

| n' ⇒ string_of_nat_aux time' n' acc'

end

end.

Definition string_of_nat (n : nat) : string :=

string_of_nat_aux n n "".

#[export] Instance showNat : Show nat :=

{

show := string_of_nat

}.

Compute (show 42).

let d := match n mod 10 with

| 0 ⇒ "0" | 1 ⇒ "1" | 2 ⇒ "2" | 3 ⇒ "3" | 4 ⇒ "4" | 5 ⇒ "5"

| 6 ⇒ "6" | 7 ⇒ "7" | 8 ⇒ "8" | _ ⇒ "9"

end in

let acc' := d ++ acc in

match time with

| 0 ⇒ acc'

| S time' ⇒

match n / 10 with

| 0 ⇒ acc'

| n' ⇒ string_of_nat_aux time' n' acc'

end

end.

Definition string_of_nat (n : nat) : string :=

string_of_nat_aux n n "".

#[export] Instance showNat : Show nat :=

{

show := string_of_nat

}.

Compute (show 42).

(* FILL IN HERE *)

☐

☐

Definition showOne {A : Type} `{Show A} (a : A) : string :=

"The value is " ++ show a.

Compute (showOne true).

Compute (showOne 42).

"The value is " ++ show a.

Compute (showOne true).

Compute (showOne 42).

The parameter `{Show A} is a
Concretely, this constraint should be thought of as an extra
parameter to showOne supplying
More interestingly, a single function can come with multiple class
constraints:

*class constraint*, which states that the function showOne is expected to be applied only to types A that belong to the Show class.*evidence*that A is an instance of Show -- i.e., it is essentially just a show function for A, which is implicitly invoked by the expression show a.
Definition showTwo {A B : Type}

`{Show A} `{Show B} (a : A) (b : B) : string :=

"First is " ++ show a ++ " and second is " ++ show b.

Compute (showTwo true 42).

Compute (showTwo Red Green).

`{Show A} `{Show B} (a : A) (b : B) : string :=

"First is " ++ show a ++ " and second is " ++ show b.

Compute (showTwo true 42).

Compute (showTwo Red Green).

In the body of showTwo, the type of the argument to each
instance of show determines which of the implicitly supplied
show functions (for A or B) gets invoked.
Of course, Show is not the only interesting typeclass. There
are many other situations where it is useful to be able to
choose (and construct) specific functions depending on the type of
an argument that is supplied to a generic function like show.
Another typical example is equality checkers.
Here is another basic example of typeclasses: a class Eq
describing types with a (boolean) test for equality.

#### Exercise: 1 star, standard (missingConstraint)

What happens if we forget the class constraints in the definitions of showOne or showTwo? Try deleting them and see what happens. ☐
And here are some basic instances:

#[export] Instance eqBool : Eq bool :=

{

eqb := fun (b c : bool) ⇒

match b, c with

| true, true ⇒ true

| true, false ⇒ false

| false, true ⇒ false

| false, false ⇒ true

end

}.

#[export] Instance eqNat : Eq nat :=

{

eqb := Nat.eqb

}.

{

eqb := fun (b c : bool) ⇒

match b, c with

| true, true ⇒ true

| true, false ⇒ false

| false, true ⇒ false

| false, false ⇒ true

end

}.

#[export] Instance eqNat : Eq nat :=

{

eqb := Nat.eqb

}.

One possible confusion should be addressed here: Why should we
need to define a typeclass for boolean equality when Coq's

*propositional*equality (x = y) is completely generic? The answer is that, while it makes sense to*claim*that two values x and y are equal no matter what their type is, it is not possible to write a decidable equality*checker*for arbitrary types. In particular, equality at types like nat→nat is undecidable.#### Exercise: 3 stars, standard, optional (boolArrowBool)

There are some function types, like bool→bool, for which checking equality makes perfect sense. Write an Eq instance for this type.
(* FILL IN HERE *)

☐

☐

## Parameterized Instances: New Typeclasses from Old

#[export] Instance showPair {A B : Type} `{Show A} `{Show B} : Show (A × B) :=

{

show p :=

let (a,b) := p in

"(" ++ show a ++ "," ++ show b ++ ")"

}.

Compute (show (true,42)).

{

show p :=

let (a,b) := p in

"(" ++ show a ++ "," ++ show b ++ ")"

}.

Compute (show (true,42)).

Similarly, here is an Eq instance for pairs...

#[export] Instance eqPair {A B : Type} `{Eq A} `{Eq B} : Eq (A × B) :=

{

eqb p

let (p1a,p1b) := p

let (p2a,p2b) := p

andb (p1a =? p2a) (p1b =? p2b)

}.

{

eqb p

_{1}p_{2}:=let (p1a,p1b) := p

_{1}inlet (p2a,p2b) := p

_{2}inandb (p1a =? p2a) (p1b =? p2b)

}.

...and here is Show for lists:

Fixpoint showListAux {A : Type} (s : A → string) (l : list A) : string :=

match l with

| nil ⇒ ""

| cons h nil ⇒ s h

| cons h t ⇒ append (append (s h) ", ") (showListAux s t)

end.

#[export] Instance showList {A : Type} `{Show A} : Show (list A) :=

{

show l := append "[" (append (showListAux show l) "]")

}.

match l with

| nil ⇒ ""

| cons h nil ⇒ s h

| cons h t ⇒ append (append (s h) ", ") (showListAux s t)

end.

#[export] Instance showList {A : Type} `{Show A} : Show (list A) :=

{

show l := append "[" (append (showListAux show l) "]")

}.

#### Exercise: 3 stars, standard (eqEx)

Write an Eq instance for lists and Show and Eq instances for the option type constructor.
(* FILL IN HERE *)

☐

☐

#### Exercise: 3 stars, standard, optional (boolArrowA)

Generalize your solution to the boolArrowBool exercise to build an equality instance for any type of the form bool→A, where A itself is an Eq type. Show that it works for bool→bool→nat.
(* FILL IN HERE *)

☐

☐

## Class Hierarchies

The reason this is bad is because we now need to use a new
equality operator (eqbad) if we want to test for equality on
ordered values.

Definition lt {A: Type} `{Eq A} `{OrdBad A} (x y : A) : bool :=

andb (lebad x y) (negb (eqbad x y)).

andb (lebad x y) (negb (eqbad x y)).

A much better way is to parameterize the definition of Ord on an
Eq class constraint:

Class Ord A `{Eq A} : Type :=

{

le : A → A → bool

}.

Notation "x <=? y" := (le x y) (at level 70).

Check Ord.

{

le : A → A → bool

}.

Notation "x <=? y" := (le x y) (at level 70).

Check Ord.

(The old class Eq is sometimes called a "superclass" of Ord,
but, again, this terminology is potentially confusing: Try to
avoid thinking about analogies with object-oriented
programming!)
When we define instances of Ord, we just have to implement the
le operation.

Functions expecting to be instantiated with an instance of Ord
now have two class constraints, one witnessing that they have an
associated eqb operation, and one for le.

#### Exercise: 1 star, standard (missingConstraintAgain)

What does Coq say if the Ord class constraint is left out of the definition of max? What about the Eq class constraint? ☐#### Exercise: 3 stars, standard (ordMisc)

Define Ord instances for options and pairs.
(* FILL IN HERE *)

☐

☐

(* FILL IN HERE *)

☐

☐

# How It Works

## Implicit Generalization

*implicit generalization*, that was added to Coq to support typeclasses but that can also be used to good effect elsewhere.

Generalizable Variables A.

By default, Coq only implicitly generalizes variables declared in
this way, to avoid puzzling behavior in case of typos. There is
also a Generalize Variables All command, but it's probably not a
good idea to use it!
Now, for example, we can shorten the declaration of the showOne
function by omitting the binding for A at the front.

Coq will notice that the occurrence of A inside the `{...} is
unbound and automatically insert the binding that we wrote
explicitly before.

Print showOne1.

(* ==>

showOne1 =

fun (A : Type) (H : Show A) (a : A) => "The value is " ++ show a

: forall A : Type, Show A -> A -> string

Arguments A, H are implicit and maximally inserted

*)

(* ==>

showOne1 =

fun (A : Type) (H : Show A) (a : A) => "The value is " ++ show a

: forall A : Type, Show A -> A -> string

Arguments A, H are implicit and maximally inserted

*)

The "implicit and maximally generalized" annotation on the last
line means that the automatically inserted bindings are treated as
if they had been written with {...}, rather than (...). The
"implicit" part means that the type argument A and the Show
witness H are usually expected to be left implicit: whenever we
write showOne1, Coq will automatically insert two unification
variables as the first two arguments. This automatic insertion
can be disabled by writing @, so a bare occurrence of showOne1
means the same as @showOne1 _ _. The "maximally inserted" part
says that these arguments should inserted automatically even when
there is no following explicit argument.
In fact, even the `{Show A} form hides one bit of implicit
generalization: the bound name of the Show constraint itself.
You will sometimes see class constraints written more explicitly,
like this...

... or even like this:

The advantage of the latter form is that it gives a name that can
be used, in the body, to explicitly refer to the supplied evidence
for Show A. This can be useful when things get complicated and
you want to make your code more explicit so you can better
understand and control what's happening.
We can actually go one bit further and omit A altogether, with
no change in meaning (though, again, this may be more confusing
than helpful):

If we ask Coq to print the arguments that are normally implicit,
we see that all these definitions are exactly the same
internally.

Set Printing Implicit.

Print showOne.

Print showOne1.

Print showOne2.

Print showOne3.

Print showOne4.

(* ==>

showOne =

fun (A : Type) (H : Show A) (a : A) =>

"The value is " ++ @show A H a

: forall A : Type, Show A -> A -> string

*)

Unset Printing Implicit.

Print showOne.

Print showOne1.

Print showOne2.

Print showOne3.

Print showOne4.

(* ==>

showOne =

fun (A : Type) (H : Show A) (a : A) =>

"The value is " ++ @show A H a

: forall A : Type, Show A -> A -> string

*)

Unset Printing Implicit.

The examples we've seen so far illustrate how implicit
generalization works, but you may not be convinced yet that it is
actually saving enough keystrokes to be worth the trouble of
adding such a fancy mechanism to Coq. Where things become more
convincing is when classes are organized into hierarchies. For
example, here is an alternate definition of the max function:

If we print out max1 in full detail, we can see that the
implicit generalization around `{Ord A} led Coq to fill in not
only a binding for A but also a binding for H, which it can
see must be of type Eq A because it appears as the second
argument to Ord. (And why is Ord applied here to two
arguments instead of just the one, A, that we wrote? Because
Ord's arguments are maximally inserted!)

Set Printing Implicit.

Print max1.

(* ==>

max1 =

fun (A : Type) (H : Eq A) (H

if @le A H H

: forall (A : Type) (H : Eq A),

@Ord A H -> A -> A -> A

*)

Check Ord.

(* ==> Ord : forall A : Type, Eq A -> Type *)

Unset Printing Implicit.

Print max1.

(* ==>

max1 =

fun (A : Type) (H : Eq A) (H

_{0}: @Ord A H) (x y : A) =>if @le A H H

_{0}x y then y else x: forall (A : Type) (H : Eq A),

@Ord A H -> A -> A -> A

*)

Check Ord.

(* ==> Ord : forall A : Type, Eq A -> Type *)

Unset Printing Implicit.

For completeness, a couple of final points about implicit
generalization. First, it can be used in situations where no
typeclasses at all are involved. For example, we can use it to
write quantified propositions mentioning free variables, following
the common informal convention that these are to be quantified
implicitly.

Generalizable Variables x y.

Lemma commutativity_property : `{x + y = y + x}.

Proof. intros. lia. Qed.

Check commutativity_property.

Lemma commutativity_property : `{x + y = y + x}.

Proof. intros. lia. Qed.

Check commutativity_property.

The previous examples have all shown implicit generalization being
used to fill in forall binders. It will also create fun
binders, when this makes sense:

Defining a function in this way is not very natural, however. In
particular, the arguments are all implicit and maximally
inserted (as can be seen if we print out its definition)...

... so we will need to use @ to actually apply the function:

(* Compute (implicit_fun 2 3). *)

(* ==>

Error: Illegal application (Non-functional construction):

The expression "implicit_fun" of type "nat"

cannot be applied to the term

"2" : "nat"

*)

Compute (@implicit_fun 2 3).

(* ==>

Error: Illegal application (Non-functional construction):

The expression "implicit_fun" of type "nat"

cannot be applied to the term

"2" : "nat"

*)

Compute (@implicit_fun 2 3).

Writing `(...), with parentheses instead of curly braces, causes
Coq to perform the same implicit generalization step, but does

*not*mark the inserted binders themselves as implicit.## Records are Products

Internally, this declaration is desugared into a single-field
inductive type, roughly like this:

Inductive Point : Set :=

| Build_Point : nat → nat → Point.
Elements of this type can be built, if we like, by applying the
Build_Point constructor directly.

Inductive Point : Set :=

| Build_Point : nat → nat → Point.

Or we can use more familar record syntax, which allows us to name
the fields and write them in any order:

We can also access fields of a record using conventional "dot notation"
(with slightly clunky concrete syntax):

Record declarations can also be parameterized:

(Note that the field names have to be different. Any given field
name can belong to only one record type. This greatly simplifies
type inference!)

Check {| lx:=2; ly:=4; label:="hello" |}.

(* ==>

{| lx := 2; ly := 4; label := "hello" |}

: LabeledPoint string

*)

(* ==>

{| lx := 2; ly := 4; label := "hello" |}

: LabeledPoint string

*)

#### Exercise: 1 star, standard (rcdParens)

Note that the A parameter in the definition of LabeledPoint is bound with parens, not curly braces. Why is this a better choice? ☐## Typeclasses are Records

Set Printing All.

Print Show.

(* ==>

Record Show (A : Type) : Type :=

Build_Show

{ show : A -> string }

*)

Unset Printing All.

Print Show.

(* ==>

Record Show (A : Type) : Type :=

Build_Show

{ show : A -> string }

*)

Unset Printing All.

(If you run the Print command yourself, you'll see that Show
actually displays as a Variant; this is Coq's terminology for a
single-field record.)
Analogously, Instance declarations become record values:

Note that the syntax for record values is slightly different from
Instance declarations. Record values are written with
curly-brace-vertical-bar delimiters, while Instance declarations
are written here with just curly braces. (To be precise, both
forms of braces are actually allowed for Instance declarations,
and either will work in most situations; however, type inference
sometimes works a bit better with bare curly braces.)
Similarly, overloaded functions like show are really just record
projections, which in turn are just functions that select a
particular argument of a one-constructor Inductive type.

Set Printing All.

Print show.

(* ==>

show =

fun (A : Type) (Show0 : Show A) =>

match Show0 with

| Build_Show _ show => show

end

: forall (A : Type), Show A -> A -> string

Arguments A, Show are implicit and maximally inserted *)

Unset Printing All.

Print show.

(* ==>

show =

fun (A : Type) (Show0 : Show A) =>

match Show0 with

| Build_Show _ show => show

end

: forall (A : Type), Show A -> A -> string

Arguments A, Show are implicit and maximally inserted *)

Unset Printing All.

## Inferring Instances

How does this happen?
First, since the arguments to show are marked implicit, what we
typed is automatically expanded to @show _ _ 42. The first _
should obviously be replaced by nat. But what about the second?
By ordinary type inference, Coq knows that, to make the whole
expression well typed, the second argument to @show must be a
value of type Show nat. It attempts to find or construct such a
value using a variant of the eauto proof search procedure that
refers to a "hint database" called typeclass_instances.

#### Exercise: 1 star, standard (HintDb)

Uncomment and execute the following command. Search for "For Show" in the output and have a look at the entries for showNat and showPair.
(* Print HintDb typeclass_instances. *)

☐

☐

Set Typeclasses Debug.

Check (show 42).

(* ==>

Debug: 1: looking for (Show nat) without backtracking

Debug: 1.1: exact showNat on (Show nat), 0 subgoal(s)

*)

Check (show 42).

(* ==>

Debug: 1: looking for (Show nat) without backtracking

Debug: 1.1: exact showNat on (Show nat), 0 subgoal(s)

*)

In this simple example, the proof search succeeded immediately
because showNat was in the hint database. In more interesting
cases, the proof search needs to try to assemble an

*expression*of appropriate type using both functions and constants from the hint database. (This is very like what happens when proof search is used as a tactic to automatically assemble compound proofs by combining theorems from the environment.)
Check (show (true,42)).

(* ==>

Debug: 1: looking for (Show (bool * nat)) without backtracking

Debug: 1.1: simple apply @showPair on (Show (bool * nat)), 2 subgoal(s)

Debug: 1.1.3 : (Show bool)

Debug: 1.1.3: looking for (Show bool) without backtracking

Debug: 1.1.3.1: exact showBool on (Show bool), 0 subgoal(s)

Debug: 1.1.3 : (Show nat)

Debug: 1.1.3: looking for (Show nat) without backtracking

Debug: 1.1.3.1: exact showNat on (Show nat), 0 subgoal(s) *)

Unset Typeclasses Debug.

(* ==>

Debug: 1: looking for (Show (bool * nat)) without backtracking

Debug: 1.1: simple apply @showPair on (Show (bool * nat)), 2 subgoal(s)

Debug: 1.1.3 : (Show bool)

Debug: 1.1.3: looking for (Show bool) without backtracking

Debug: 1.1.3.1: exact showBool on (Show bool), 0 subgoal(s)

Debug: 1.1.3 : (Show nat)

Debug: 1.1.3: looking for (Show nat) without backtracking

Debug: 1.1.3.1: exact showNat on (Show nat), 0 subgoal(s) *)

Unset Typeclasses Debug.

In the second line, the search procedure decides to try applying
showPair, from which it follows (after a bit of unification)
that it needs to find an instance of Show Nat and an instance of
Show Bool, each of which succeeds immediately as before.
In summary, here are the steps again:

show 42

===> { Implicit arguments }

@show _ _ 42

===> { Typing }

@show (?A : Type) (?Show0 : Show ?A) 42

===> { Unification }

@show nat (?Show0 : Show nat) 42

===> { Proof search for Show Nat returns showNat }

@show nat showNat 42
Since programs and proofs in Coq are fundamentally made from the
same stuff, the mechanisms of typeclasses extend smoothly to
situations where classes contain not only data and functions but
also proofs.
This is a big topic -- too big for a basic tutorial -- but let's
take a quick look at a few things.
The Eq typeclass defines a single overloaded function that tests
for equality between two elements of some type. We can extend
this to a subclass that also comes with a proof that the given
equality tester is correct, in the sense that, whenever it returns
true, the two values are actually equal in the propositional
sense (and vice versa).

show 42

===> { Implicit arguments }

@show _ _ 42

===> { Typing }

@show (?A : Type) (?Show0 : Show ?A) 42

===> { Unification }

@show nat (?Show0 : Show nat) 42

===> { Proof search for Show Nat returns showNat }

@show nat showNat 42

# Typeclasses and Proofs

## Propositional Typeclass Members

To build an instance of EqDec, we must now supply an appropriate
proof.

If we do not happen to have an appropriate proof already in the
environment, we can simply omit it. Coq will enter
proof mode and ask the user to use tactics to construct
inhabitants for the fields.

#[export] Instance eqdecBool' : EqDec bool.

Proof.

constructor.

intros x y. destruct x; destruct y; simpl; unfold iff; auto.

Defined.

Proof.

constructor.

intros x y. destruct x; destruct y; simpl; unfold iff; auto.

Defined.

Given a typeclass with propositional members, we can use these
members in proving things involving this typeclass.
Here, for example, is a quick (and somewhat contrived)
example of a proof of a property that holds for arbitrary values
from the EqDec class...

Lemma eqb_fact `{EqDec A} : ∀ (x y z : A),

x =? y = true → y =? z = true → x = z.

Proof.

intros x y z Exy Eyz.

rewrite eqb_eq in Exy.

rewrite eqb_eq in Eyz.

subst. reflexivity. Qed.

x =? y = true → y =? z = true → x = z.

Proof.

intros x y z Exy Eyz.

rewrite eqb_eq in Exy.

rewrite eqb_eq in Eyz.

subst. reflexivity. Qed.

There is much more to say about how typeclasses can be used (and
how they should not be used) to support large-scale proofs in Coq.
See the suggested readings below.
Naturally, it is also possible to have typeclass instances as
members of other typeclasses: these are called

## Substructures

*substructures*. Here is an example adapted from the Coq Reference Manual.
From Coq Require Import Relations.Relation_Definitions.

Class Reflexive (A : Type) (R : relation A) :=

{

reflexivity : ∀ x, R x x

}.

Class Transitive (A : Type) (R : relation A) :=

{

transitivity : ∀ x y z, R x y → R y z → R x z

}.

Generalizable Variables z w R.

Lemma trans3 : ∀ `{Transitive A R},

`{R x y → R y z → R z w → R x w}.

Proof.

intros.

apply (transitivity x z w). apply (transitivity x y z).

assumption. assumption. assumption. Defined.

Class PreOrder (A : Type) (R : relation A) :=

{ PreOrder_Reflexive :> Reflexive A R ;

PreOrder_Transitive :> Transitive A R }.

Class Reflexive (A : Type) (R : relation A) :=

{

reflexivity : ∀ x, R x x

}.

Class Transitive (A : Type) (R : relation A) :=

{

transitivity : ∀ x y z, R x y → R y z → R x z

}.

Generalizable Variables z w R.

Lemma trans3 : ∀ `{Transitive A R},

`{R x y → R y z → R z w → R x w}.

Proof.

intros.

apply (transitivity x z w). apply (transitivity x y z).

assumption. assumption. assumption. Defined.

Class PreOrder (A : Type) (R : relation A) :=

{ PreOrder_Reflexive :> Reflexive A R ;

PreOrder_Transitive :> Transitive A R }.

The syntax :> indicates that each PreOrder can be seen as a
Reflexive and Transitive relation, so that, any time a
reflexive relation is needed, a preorder can be used instead.

Lemma trans3_pre : ∀ `{PreOrder A R},

`{R x y → R y z → R z w → R x w}.

Proof. intros. eapply trans3; eassumption. Defined.

`{R x y → R y z → R z w → R x w}.

Proof. intros. eapply trans3; eassumption. Defined.

# Some Useful Typeclasses

## Dec

Require Import ssreflect ssrbool.

Print decidable.

(* ==>

decidable = fun P : Prop => {P} + {~ P}

*)

Print decidable.

(* ==>

decidable = fun P : Prop => {P} + {~ P}

*)

... where {P} + {~ P} is an "informative disjunction" of P and
¬P.
It is easy to wrap this in a typeclass of "decidable
propositions":

We can now create instances encoding the information that
propositions of various forms are decidable. For example, the
proposition x = y is decidable (for any specific x and y),
assuming that x and y belong to a type with an EqDec
instance.

#[export] Instance EqDec__Dec {A} `{H : EqDec A} (x y : A) : Dec (x = y).

Proof.

constructor.

unfold decidable.

destruct (x =? y) eqn:E.

- left. rewrite <- eqb_eq. assumption.

- right. intros C. rewrite <- eqb_eq in C. rewrite E in C. inversion C.

Defined.

Proof.

constructor.

unfold decidable.

destruct (x =? y) eqn:E.

- left. rewrite <- eqb_eq. assumption.

- right. intros C. rewrite <- eqb_eq in C. rewrite E in C. inversion C.

Defined.

Similarly, we can lift decidability through logical operators like
conjunction:

#[export] Instance Dec_conj {P Q} {H : Dec P} {I : Dec Q} : Dec (P ∧ Q).

Proof.

constructor. unfold decidable.

destruct H as [D]; destruct D;

destruct I as [D]; destruct D; auto;

right; intro; destruct H; contradiction.

Defined.

Proof.

constructor. unfold decidable.

destruct H as [D]; destruct D;

destruct I as [D]; destruct D; auto;

right; intro; destruct H; contradiction.

Defined.

#### Exercise: 3 stars, standard (dec_neg_disj)

Give instance declarations showing that, if P and Q are decidable propositions, then so are ¬P and P∨Q.
(* FILL IN HERE *)

☐

☐

#### Exercise: 4 stars, standard (Dec_All)

The following function converts a list into a proposition claiming that every element of that list satiesfies some proposition P:
Fixpoint All {T : Type} (P : T → Prop) (l : list T) : Prop :=

match l with

| [] ⇒ True

| x :: l' ⇒ P x ∧ All P l'

end.

match l with

| [] ⇒ True

| x :: l' ⇒ P x ∧ All P l'

end.

Create an instance of Dec for All P l, given that P a is
decidable for every a.

(* FILL IN HERE *)

☐

☐

Now we don't need to remember that, for example, the test for
equality on numbers is called eqb, because instead of this...

Definition silly_fun1 (x y z : nat) :=

if andb (x =? y) (andb (y =? z) (x =? z))

then "all equal"

else "not all equal".

if andb (x =? y) (andb (y =? z) (x =? z))

then "all equal"

else "not all equal".

... we can just write this:

Definition silly_fun2 (x y z : nat) :=

if (x = y ∧ y = z ∧ x = z)?

then "all equal"

else "not all equal".

if (x = y ∧ y = z ∧ x = z)?

then "all equal"

else "not all equal".

## Monad

- input / output
- state mutation
- failure
- nondeterminism
- randomness
- etc.

Require Export ExtLib.Structures.Monads.

Export MonadNotation.

Open Scope monad_scope.

Export MonadNotation.

Open Scope monad_scope.

The main definition provided by this library is the following typeclass:

Class Monad (M : Type → Type) : Type :=

{

ret : ∀ {T : Type}, T → M T ;

bind : ∀ {T U : Type}, M T → (T → M U) → M U

}. That is, a type family M is an instance of the Monad class if we can define functions ret and bind of the appropriate types. (If you Print the actual definition, you'll see something more complicated, involving Polymorphic Record bla bla... The Polymorphic part refers to Coq's "universe polymorphism," which does not concern us here.)
For example, we can define a monad instance for option like
this:

Class Monad (M : Type → Type) : Type :=

{

ret : ∀ {T : Type}, T → M T ;

bind : ∀ {T U : Type}, M T → (T → M U) → M U

}. That is, a type family M is an instance of the Monad class if we can define functions ret and bind of the appropriate types. (If you Print the actual definition, you'll see something more complicated, involving Polymorphic Record bla bla... The Polymorphic part refers to Coq's "universe polymorphism," which does not concern us here.)

#[export] Instance optionMonad : Monad option :=

{

ret T x :=

Some x ;

bind T U m f :=

match m with

None ⇒ None

| Some x ⇒ f x

end

}.

{

ret T x :=

Some x ;

bind T U m f :=

match m with

None ⇒ None

| Some x ⇒ f x

end

}.

The other nice thing we get from the Monad library is
lightweight notation for bind: Instead of

bind m

x <- m

bind m

m
This allows us to write functions involving "option plumbing" very
compactly.
For example, suppose we have a function that looks up the nth
element of a list, returning None if the list contains less than
n elements.

bind m

_{1}(fun x ⇒ m_{2}), we can writex <- m

_{1};; m_{2}. Or, if the result from m_{1}is not needed in m_{2}, then instead ofbind m

_{1}(fun _ ⇒ m_{2}), we can writem

_{1};; m_{2}.
Fixpoint nth_opt {A : Type} (n : nat) (l : list A) : option A :=

match l with

[] ⇒ None

| h::t ⇒ if n =? 0 then Some h else nth_opt (n-1) t

end.

match l with

[] ⇒ None

| h::t ⇒ if n =? 0 then Some h else nth_opt (n-1) t

end.

We can write a function that sums the first three elements of a
list (returning None if the list is too short) like this:

Definition sum3 (l : list nat) : option nat :=

x

x

x

ret (x

x

_{0}<- nth_opt 0 l ;;x

_{1}<- nth_opt 1 l ;;x

_{2}<- nth_opt 2 l ;;ret (x

_{0}+ x_{1}+ x_{2}).
One final convenience for programming with monads is a collection
of operators for "lifting" functions on ordinary values to
functions on monadic computations. ExtLib defines three -- one
for unary functions, one for binary, and one for ternary. The
definitions (slightly simplified) look like this:

Definition liftM

{m : Type → Type}

{M : Monad m}

{T U : Type} (f : T → U)

: m T → m U :=

fun x ⇒ bind x (fun x ⇒ ret (f x)).

Definition liftM2

{m : Type → Type}

{M : Monad m}

{T U V : Type} (f : T → U → V)

: m T → m U → m V :=

fun x y ⇒ bind x (fun x ⇒ liftM (f x) y).

Definition liftM3

{m : Type → Type}

{M : Monad m}

{T U V W : Type} (f : T → U → V → W)

: m T → m U → m V → m W :=

fun x y z ⇒ bind x (fun x ⇒ liftM2 (f x) y z).

{m : Type → Type}

{M : Monad m}

{T U : Type} (f : T → U)

: m T → m U :=

fun x ⇒ bind x (fun x ⇒ ret (f x)).

Definition liftM2

{m : Type → Type}

{M : Monad m}

{T U V : Type} (f : T → U → V)

: m T → m U → m V :=

fun x y ⇒ bind x (fun x ⇒ liftM (f x) y).

Definition liftM3

{m : Type → Type}

{M : Monad m}

{T U V W : Type} (f : T → U → V → W)

: m T → m U → m V → m W :=

fun x y z ⇒ bind x (fun x ⇒ liftM2 (f x) y z).

For example, suppose we have two option nats and we would like
to calculate their sum (unless one of them is None, in which
case we want None). Instead of this...

Definition sum3opt (n

x

x

ret (x

_{1}n_{2}: option nat) :=x

_{1}<- n_{1};;x

_{2}<- n_{2};;ret (x

_{1}+ x_{2}).
...we can use liftM2 to write it more compactly:

The /examples directory in the ext-lib Github
repository (https://github.com/coq-community/coq-ext-lib/blob/master/)includes
some further examples of using monads in Coq.
Two popular typeclasses from the Coq standard library are
Equivalence (and the associated classes Reflexive,
Transitive, etc.) and Proper. They are described in the
second half of
A much larger collection of typeclasses for formalizing
mathematics is described in

## Others

*A Gentle Introduction to Type Classes and Relations in Coq*, by Castéran and Sozeau. https://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf.*Type Classes for Mathematics in Type Theory*, by Bas Spitters and Eelis van der Weegen. https://arxiv.org/pdf/1102.1323.pdf
... says that it works for any Eq type. Naturally, we can use
it in a definition like this...

... and then we can apply foo to arguments of any Eq type.
Right?

Fail Check (foo true).

(* ==>

The command has indeed failed with message:

The term "true" has type "bool" while it is expected

to have type "bool -> bool". *)

(* ==>

The command has indeed failed with message:

The term "true" has type "bool" while it is expected

to have type "bool -> bool". *)

Huh?!
Here's what happened:
The lesson is that it matters a great deal
One of the ways in which Coq's typeclasses differ most from
Haskell's is the lack, in Coq, of an automatic check for
"overlapping instances."
That is, it is completely legal to define a given type to be an
instance of a given class in two different ways.

- When we defined foo, the type of x was not specified, so Coq filled in a unification variable (an "evar") ?A.
- When typechecking the expression eqb x, the typeclass instance mechanism was asked to search for a type-correct instance of Eq, i.e., an expression of type Eq ?A.
- This search immediately succeeded because the first thing it tried worked; this happened to be the constant eqBoolBool : Eq (bool→bool). In the process, ?A got instantiated to bool→bool.
- The type calculated for foo was therefore (bool→bool)->(bool→bool)->bool.

*exactly*what problems are posed to the instance search engine.#### Exercise: 1 star, standard (debugDefaulting)

Do Set Typeclasses Debug and verify that this is what happened. ☐## Manipulating the Hint Database

Inductive baz := Baz : nat → baz.

#[export] Instance baz1 : Show baz :=

{

show b :=

match b with

Baz n ⇒ "Baz: " ++ show n

end

}.

#[export] Instance baz2 : Show baz :=

{

show b :=

match b with

Baz n ⇒ "[" ++ show n ++ " is a Baz]"

end

}.

Compute (show (Baz 42)).

(* ==>

= "42 is a Baz"

: string *)

#[export] Instance baz1 : Show baz :=

{

show b :=

match b with

Baz n ⇒ "Baz: " ++ show n

end

}.

#[export] Instance baz2 : Show baz :=

{

show b :=

match b with

Baz n ⇒ "[" ++ show n ++ " is a Baz]"

end

}.

Compute (show (Baz 42)).

(* ==>

= "42 is a Baz"

: string *)

When this happens, it is unpredictable which instance will be
found first by the instance search process; here it just happened
to be the second. The reason Coq doesn't do the overlapping
instances check is because its type system is much more complex
than Haskell's -- so much so that it is very challenging in
general to decide whether two given instances overlap.
The reason this is unfortunate is that, in more complex
situations, it may not be obvious when there are overlapping
instances.
One way to deal with overlapping instances is to "curate" the hint
database by explicitly adding and removing specific instances.
To remove things, use Remove Hints.
Once again, local, global, and export pragmas ca apply:

#[export] Remove Hints baz1 baz2 : typeclass_instances.

To add them back (or to add arbitrary constants that have the
right type to be intances -- i.e., their type ends with an applied
typeclass -- but that were not created by Instance declarations),
use Existing Instance:

#[export] Existing Instance baz1.

Compute (show (Baz 42)).

(* ==>

= "Baz: 42"

: string *)

#[export] Remove Hints baz1 : typeclass_instances.

Compute (show (Baz 42)).

(* ==>

= "Baz: 42"

: string *)

#[export] Remove Hints baz1 : typeclass_instances.

Another way of controlling which instances are chosen by proof
search is to assign

*priorities*to overlapping instances:
#[export] Instance baz3 : Show baz | 2 :=

{

show b :=

match b with

Baz n ⇒ "Use me first! " ++ show n

end

}.

#[export] Instance baz4 : Show baz | 3 :=

{

show b :=

match b with

Baz n ⇒ "Use me second! " ++ show n

end

}.

Compute (show (Baz 42)).

(* ==>

= "Use me first! 42"

: string *)

{

show b :=

match b with

Baz n ⇒ "Use me first! " ++ show n

end

}.

#[export] Instance baz4 : Show baz | 3 :=

{

show b :=

match b with

Baz n ⇒ "Use me second! " ++ show n

end

}.

Compute (show (Baz 42)).

(* ==>

= "Use me first! 42"

: string *)

0 is the highest priority.
If the priority is not specified, it defaults to the number of
binders of the instance. (This means that more specific -- less
polymorphic -- instances will be chosen over less specific
ones.)
Existing Instance declarations can also be given explicit
priorities.

# Debugging

## Instantiation Failures

Inductive bar :=

Bar : nat → bar.

Fail Definition eqBar :=

(Bar 42) =? (Bar 43).

(* ===>

The command has indeed failed with message:

Unable to satisfy the following constraints:

?Eq : "Eq bar" *)

Fail Definition ordBarList :=

le [Bar 42] [Bar 43].

(* ===>

The command has indeed failed with message:

Unable to satisfy the following constraints:

?H : "Eq (list bar)"

?Ord : "Ord (list bar)" *)

Bar : nat → bar.

Fail Definition eqBar :=

(Bar 42) =? (Bar 43).

(* ===>

The command has indeed failed with message:

Unable to satisfy the following constraints:

?Eq : "Eq bar" *)

Fail Definition ordBarList :=

le [Bar 42] [Bar 43].

(* ===>

The command has indeed failed with message:

Unable to satisfy the following constraints:

?H : "Eq (list bar)"

?Ord : "Ord (list bar)" *)

In these cases, it's pretty clear what the problem is. To fix it,
we just have to define a new instance. But in more complex
situations it can be trickier.
A few simple tricks can be very helpful:
The Set Typeclasses Debug command has a variant that causes it
to print even more information: Set Typeclasses Debug Verbosity
2. Writing just Set Typeclasses Debug is equivalent to Set
Typeclasses Debug Verbosity 1.
Another potential source of confusion with error messages comes up
if you forget a `. For example:

- Do Set Printing Implicit and then use Check and Print to investigate the types of the things in the expression where the error is being reported.
- Add some @ annotations and explicitly fill in some of the arguments that should be getting instantiated automatically, to check your understanding of what they should be getting instantiated with.
- Turn on tracing of instance search with Set Typeclasses Debug.

Fail Definition max {A: Type} {Ord A} (x y : A) : A :=

if le x y then y else x.

(* ===>

The command has indeed failed with message:

Unable to satisfy the following constraints:

UNDEFINED EVARS:

?X354==A ⊢ Type (type of Ord) {?T}

?X357==A

?X358==A

if le x y then y else x.

(* ===>

The command has indeed failed with message:

Unable to satisfy the following constraints:

UNDEFINED EVARS:

?X354==A ⊢ Type (type of Ord) {?T}

?X357==A

_{0}Ord A x y ⊢ Eq A (parameter H of @le) {?H}?X358==A

_{0}Ord A x y ⊢ Ord A (parameter Ord of @le) {?Ord} *)
The UNDEFINED EVARS here is because the binders that are
automatically inserted by implicit generalization are missing.
An even more annoying way that typeclass instantiation can go
wrong is by simply diverging. Here is a small example of how this
can happen.
Declare a typeclass involving two types parameters A and B --
say, a silly typeclass that can be inhabited by arbitrary
functions from A to B:

## Nontermination

Declare instances for getting from bool to nat...

... and from nat to string:

#[export] Instance MyMap2 : MyMap nat string :=

{

mymap := fun n : nat ⇒

if le n 20 then "Pretty small" else "Pretty big"

}.

Definition e

Compute e

Definition e

Compute e

{

mymap := fun n : nat ⇒

if le n 20 then "Pretty small" else "Pretty big"

}.

Definition e

_{1}:= mymap true.Compute e

_{1}.Definition e

_{2}:= mymap 42.Compute e

_{2}.
Notice that these two instances don't automatically get us from
bool to string:

We can try to fix this by defining a generic instance that
combines an instance from A to B and an instance from B to
C:

#[export] Instance MyMap_trans {A B C : Type} `{MyMap A B} `{MyMap B C} : MyMap A C :=

{ mymap a := mymap (mymap a) }.

{ mymap a := mymap (mymap a) }.

This does get us from bool to string automatically:

However, although this example seemed to work, we are actually in
a state of great peril: If we happen to ask for an instance that
doesn't exist, the search procedure will diverge.

(*

Definition e

*)

Definition e

_{4}: list nat := mymap false.*)

#### Exercise: 1 star, standard (nonterm)

Why, exactly, did the search diverge? Enable typeclass debugging, uncomment the above Definition, and see what gets printed. (You may want to do this from the command line rather than from inside an IDE, to make it easier to kill.)# Alternative Structuring Mechanisms

- canonical structures
- bare dependent records
- modules and functors

- Assia Mahboubi and Enrico Tassi. Canonical Structures for the
working Coq user. In Sandrine Blazy, Christine Paulin, and
David Pichardie, editors, ITP 2013, 4th Conference on
Interactive Theorem Proving, volume 7998 of LNCS, pages
19–34, Rennes, France, 2013. Springer.
https://hal.inria.fr/hal-00816703v
_{1}/document - Gonthier et al., "How to make ad hoc proof automation less ad hoc", JFP 23 (4): 357–401, 2013. (This explains some weaknesses of typeclasses and why canonical structures are used in in the mathcomp libraries.)

# Advice from Experts

## Matthieu Sozeau

## John Wiegley

Typeclasses eauto := debug. and switch to my *coq* buffer to see which lookup did not resolve to the instance I was expecting. This is usually fixed by one of two things:

- Change the "priority" of the overlapping instance (something we cannot do in Haskell).
- Change the Instance to a Definition -- which I can still use it as an explicitly passed dictionary, but this removes it from resolution.

Definition foo (C D : Category) (x y : C) (f : x ~> y)

: fobj x ~> fobj y :=

fmap f. In Haskell this gives an error stating that no Functor is available. In Coq, it type checks using the highest priority C --> D functor instance in scope. I typically discover that this has happened when I try to use foo and find the Functor to be too specific, or by turning on Printing All and looking at the definition of `foo`. However, there are times when `foo` is deep down in an expression, and then it's not obvious *at all* why it's failing.

Class Foo := {

method : Type → Type

}.

Class Bar := {

bar_is_foo :> Foo

}.

Class Baz := {

baz_is_foo :> Foo

}.

Class Oops := {

oops_is_bar :> Bar

oops_is_baz :> Baz

}. Oops refers to two Foos, and I need explicit evidence to know when they are the same Foo. I work around this using indices:

Class Foo := {

method : Type → Type

}.

Class Bar (F : Foo) := {

}.

Class Baz (F : Foo) := {

}.

Class Oops (F : Foo) := {

oops_is_bar :> Bar F

oops_is_baz :> Baz F

}. Only those classes which might be multiply-inherited need to be lifted like this. It forces me to use Sections to avoid repetition, but allows Coq to see that base classes sharing is plainly evident.

A, B : Type

F : Foo

O : Oops

H : @method (@bar_is_foo (@oops_is_bar O)) A = @method F B

--------------------

@method F A = @method F B You can't apply here without simplying in H. However, what you see at first is:

A, B : Type

F : Foo

O : Oops

H : method A = method B

--------------------

method A = method B As a newcomer, knowing to turn on Printing All is just not obvious here, but it quickly becomes something you learn to do whenever what looks obvious is not.

## Michael Soegtrop

## Abhishek Anand

*always*there in Coq: typeclasses merely cuts down on verbosity because more arguments can now be implicit because they can be automatically inferred. Relying on proof search often brings predictability concerns. So, guidance on taming proof search would be very useful: Chapter 13 of Chipala's Certified Programming with Dependent Types (CPDT) might be a good background for using typeclasses. Also, it is good to keep in mind that if typeclass-resolution fails to instantiate an implicit argument, some/all of those arguments can be provided manually. Often, just providing one such implicit argument gives enough clues to the inference engine to infer all of them. I think it is important to emphasize that typeclass arguments are just implicit arguments.

_{1}.pdf.

*all*the operations (and their correctness properties) they will

*ever*need and then

*all*items in the library (say L) are parametrized by over I. A problem with this bundled approach is impossible to use

*any*part of D if you are missing

*any*operation (or proof of a logical property of the operation) in the interface I, even if parts of D don't actually need that operation: I've run into situations where it is impossible to cook up an operation that 90 percent of L doesn't use anyway. When using the unbundled approach, one can use Coq's Section mechanism to ensure that definitions/proofs only depend on items of the interface they actually use, and not on a big bundle.

# Further Reading

- How to make ad-hoc polymorphism less ad hoc Philip Wadler and Stephen Blott. 16'th Symposium on Principles of Programming Languages, ACM Press, Austin, Texas, January 1989. https://homepages.inf.ed.ac.uk/wadler/topics/type-classes.html

- Matthieu Sozeau and Nicolas Oury. First-Class Type Classes. TPHOLs 2008. https://link.springer.com/chapter/10.1007%2F978-3-540-71067-7_23

- Coq Reference Manual: https://coq.inria.fr/refman/
- Casteran and Sozeau's "Gentle Introduction": https://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf
- Sozeau's slides from a talk at Penn: https://www.cis.upenn.edu/~bcpierce/courses/670Fall12/slides.pdf

(* 2023-03-25 11:40 *)