UF IAS 2012 Archive Type classes

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:

• Sozeau First-Class Type Classes

• Type classes in the reference manual.

• Sozeau, Casteran A Tutorial on Type classes

• Spitters, van der Weegen Type Classes for Mathematics in Type Theory

• The math-classes library

• Many ideas can be gotten from the use of Canonical Structures

• Mahboubi TassiCanonical Structures for the working Coq user. (Includes a comparison between the several approaches.)

• Matita’s unification hints unify type classes and canonical structures

• For background, you may be interested in: Avigad - Type inference in mathematics