## Introduction

The aim of this project is to build theory and programs on top of abstract interfaces instead of concrete implementations. This layer of abstraction makes both proof engineering and programming more flexible: it avoids duplication of code, it introduces a canonical way to refer to operations and properties, both by names and notations, and it allows us to easily swap different implementations of number representations and their operations.

A prerequisite for this goal was to develop interfaces for:

- Algebraic hierarchy (groups, rings, fields, …)
- Relations, orders, …
- Categories, functors, universal algebra, …
- Numbers: ℕ, ℤ, ℚ, …
- Operations, (shift, power, abs, …)

Providing:

- Structure inference
- Multiple inheritance/sharing
- Convenient algebraic manipulation (e.g. rewriting)
- Idiomatic use of notations

Since all existing solutions (dependent records, packed classes (Ssreflect) and modules) suffer from drawbacks we propose a new solution: type classes! On this page we will try to explain the difficulties involved and our solutions.

## Interfaces for algebraic structures

Algebraic structures are expressed in terms of a number of carrier sets,
a number of relations and operations, and a number of laws that the
operations satisfy. One way of describing such a structure is by a
*bundled representation*: one uses a dependently-typed record that
contains the carrier, operations and laws. For example a semigroup can
be represented as follows. (The fields `sg_car`

and `sg_proper`

support
our explicit handling of naive set theory in type theory.)

Record SemiGroup : Type := { sg_car :> Setoid ; sg_op : sg_car → sg_car → sg_car ; sg_proper : Proper ((=) ==> (=) ==> (=)) sg_op ; sg_ass : ∀ x y z, sg_op x (sg_op y z) = sg_op (sg_op x y) z) }

However, this approach has some serious limitations, the most important
one being a lack of support for *sharing* components. For example,
suppose we group together two `CommutativeMonoid`

s in order to create a
`SemiRing`

. Now awkward hacks are necessary to establish equality
between the carriers. A second problem is that if we stack up these
records to represent higher structures the projection paths become
increasingly long.

Historically these problems have been an acceptable trade-off because
*unbundled representations*, in which the carrier and operations
are parameterized, introduce even more problems.

Record SemiGroup {A} (e : A → A → Prop) (sg_op : A → A → A) : Prop := { sg_proper : Proper (e ==> e ==> e) sg_op ; sg_ass : ∀ x y z, e (sg_op x (sg_op y z)) (sg_op (sg_op x y) z) }

There is nothing to bind notation to, no structure inference, and declaring and passing requires too much manual bookkeeping. Spitters and van der Weegen have proposed a use of Coq’s new type class machinery that resolves many of the problems of unbundled representations. Our current experiment confirms that this is a viable approach.

An alternative solution is provided by packed classes which use an alternative, and older, implementation of a semblance of type classes: canonical structures. Yet another approach would be to use modules. However, as these are not fist class, we would be unable to define, e.g. homomorphisms between algebraic structures.

An *operational type class* is defined for each operation and relation.

Class Equiv A := equiv: relation A. Infix "=" := equiv: type_scope. Class RingPlus A := ring_plus: A → A → A. Infix "+" := ring_plus.

Now an algebraic structure is just a type class living in `Prop`

that
is parametrized by its carrier, relations and operations. This class
contains all laws that the operations should satisfy. Since the
operations are unbundled we can easily support sharing. For example let
us consider the `SemiRing`

interface.

Class SemiRing A {e : Equiv A} {plus: RingPlus A} {mult: RingMult A} {zero: RingZero A} {one: RingOne A} : Prop := { semiring_mult_monoid :> @CommutativeMonoid A e mult one ; semiring_plus_monoid :> @CommutativeMonoid A e plus zero ; semiring_distr :> Distribute (.*.) (+) ; semiring_left_absorb :> LeftAbsorb (.*.) 0 }.

Without type classes it would be a burden to manually carry around the carrier, relations and operations. However, because these parameters are just type class instances, the type class machinery will perform that job for us. For example,

Lemma example `{SemiRing R} x : 1 * x = x + 0.

The backtick instructs Coq to automatically insert implicit
declarations, namely `e plus mult zero one`

. It also lets us omit a name
for the `SemiRing R`

parameter itself. All of these parameters will be
given automatically generated names that we will never refer to.
Furthermore, instance resolution will automatically find instances of
the operational type classes for the written notations. Thus the above
is really:

Lemma example {R e plus mult zero one} {P : @SemiRing R e plus mult zero one} x : @equiv R e (@ring_mult R mult (@ring_one R one) x) (@ring_plus R plus x (@ring_zero R zero)).

The syntax `:>`

in the definition of `SemiRing`

declares certain fields
as substructures.

## Defining instances

Proving that an actual structure is an instance of the
`SemiRing`

interface is straightforward. First we define
instances of the operational type classes.

Instance nat_equiv: Equiv nat := eq. Instance nat_plus: RingPlus nat := plus. Instance nat_0: RingZero nat := 0%nat. Instance nat_1: RingOne nat := 1%nat. Instance nat_mult: RingMult nat := mult.

Here we see that instances are just ordinary constants of the class
types. However, we use the `Instance`

keyword instead of `Definition`

to
let the type class machinery register the instance. Now, to prove that
the Peano naturals are in fact a semiring, we just write:

Instance: SemiRing nat. Proof. ... Qed.

## Example: ℕ

This approach to interfaces proved useful to formalize a standard algebraic hierarchy. For example, combined with category theory and universal algebra, ℕ and ℤ are represented as interfaces specifying an initial semiring and initial ring.

Class NaturalsToSemiRing (A : Type) := naturals_to_semiring: ∀ B `{RingMult B} `{RingPlus B} `{RingOne B} `{RingZero B}, A → B. Class Naturals A {e plus mult zero one} `{U: NaturalsToSemiRing A} := { naturals_ring :> @SemiRing A e plus mult zero one; naturals_to_semiring_mor :> ∀ `{SemiRing B}, SemiRing_Morphism (naturals_to_semiring A B); naturals_initial :> Initial (semirings.object A) }.