Type classes

Type class vs. other type/term lookup schemes:

From Avigad’s “Type inference in mathematics” and Sozeau, Casteran’s “A Gentle Introduction …”:

1. unification is used to infer implicit arguments.

2. A coercions can be inserted to resolve a type mismatch.

Record group : Type := Group {
carrier : Type;
...}
Coercion carrier : group >-> Type.

informs Coq that if it is looking for a “Type” and finds a term of type “group”, the function “carrier” can be used to produce a “Type”. Here, we’re coercing a record to a field in the record.

3. The canonical structure command inserts an entry into a database of unification hints. If Coq needs a term of the class, this can provide a unique term.

IntGroup := Group int addi zeroi negi...
Canonical Structure IntGroup.

informs Coq that if it needs a “group”, it has the option to use “IntGroup”. So, if you do something with a “group” and an integer, it will assume that you’re using the group “IntGroup”.

The problem with canonical structures is that you can only identify ONE group that uses integers.

WARNING: manual says if multiple are declared “canonical” with common fields, the first is used!

4. A type class defines both a “class” and some instances. If Coq needs a term of the class, it searches among the instances for something compatible.

Class Monoid ... := ...

and

Instance ZMult : Monoid Z_mult 1.
Instance ZAdd : Monoid Z_add 0.

informs Coq that there is a class “Monoid” and two instances. If you do something with a “Monoid” and an integer, Coq now complains that you have to say which one.

5. when all else fails, the algorithm can simplify terms or unfold definitions according to the CIC’s computational interpretation of terms, and then retry the previous steps.

Sources on type classes:

Revised on April 26, 2018 at 21:43:57 by Mike Shulman