Typeclasses and Canonical Structures

(Part of the Coq FAQ)

What are the differences between type classes and canonical structures?

There is varied opinion about when to use Typeclasses versus when to use Canonical Structures. Some references are listed below:

• Mailing list thread on Typeclasses versus Canonical Structures

• Software foundations discussion: Advice from Experts

• Canonical structures for the working Coq user: section on related work

• Packaging Mathematical Structures and Garillot's PhD thesis describe how ssreflect uses canonical structure. The thesis also has an in-depth discussion of the computational complexity "bundled" (canonical structures) and "unbundled" (typeclasses) approaches.

• How to Make Ad Hoc Proof Automation Less Ad Hoc presents a series of design patterns for canonical structure programming that enable one to carefully and predictably coax Coq’s type inference engine into triggering the execution of user-supplied algorithms during unification.

• Type Classes for Mathematics in Type Theory describes an algebraic hierarchy using type classes.

• Hints in Unification argues for a generalization of both mechanisms.

• Discussion on Discourse with many references https://coq.discourse.group/t/how-to-represent-mathematical-structures-in-coq/188/6

The mathcomp (Mathematical Components) library uses Canonical Structures, as described in the mathcomp book.

The general opinion seems to be that:

• Coq typeclasses allow multiple instances, unlike Haskell Typeclasses.
• The typeclass resolution mechanism uses more powerful unification rules and can be heavily controlled (Hint Mode, Typeclasses Opaque), but is also harder to predict.
• Debugging typeclasses is harder due to their greater power (in particular, Hint Extern). On the other hand, there is Set Typeclasses Debug (and Set Typeclasses Debug Verbosity 2); no similar mechanism exists for canonical structures.
• Typeclass resolution can be slow in large developments, and typeclasses can lead to huge terms because of redundancy in class indices.
• Canonical structures are simple and their unification rule is easy to reason about. However, the way they are triggered by projections can be hard to understand, whereas typeclasses can be explained as "just" an inference mechanism that fills holes.

Debugging

See https://github.com/coq/coq/wiki/Troubleshooting#what-can-i-do-when-setoid_rewrite-hangs