The algebraic hierarchy using type classes in type theory

jww Eelis van der Weegen.

We propose generic design patterns to organize algebraic structures using type classes inside the Coq system. We support multiple inheritance, sharing of notations and theories, and automated structure inference. A library for many-sorted universal algebra abstracts from the specific algebraic structures and aids the organization of the library. Category theory provides a further useful abstraction. We provide abstract interfaces for N, Z, Q as the initial semiring, the initial ring and a field of fractions. Similarly, we provide an interface for polynomials over a ring R using R-algebras. We show that the standard implementations of these are in fact instances of these type classes.

Finally, we use type classes to conveniently implement a quote function using the Prolog-like abilities of type class unification. We integrate this with our development of universal algebra.