refining types with modules and typeclasses

Question

I'm not very familiar with modules or typeclasses in Coq, but based on my basic understanding of them, I believe I have a problem where I should use them.

I want to define a sum function that adds all the elements of a polymorphic list t. It should only work when the type of elements of the list (t) has some definition for plus_function and plus_id_element. The definition of sum I'd like to write would be something like this:

Fixpoint sum {t : Type} (l : list t) :=
  match l with
  | Nil => plus_id_element t
  | Cons x xs => ((plus_function t) x (sum xs))
  end.

I don't know what's the usual way to achieve something like this in Coq. I believe in Idris, for example, one would replace t by an interface/typeclass that defines plus_function and plus_id_element. Although typeclasses exist in Coq, I haven't seen them used very often and I believe people usually use modules instead to achieve something similar. I'm not sure if I'm mixing unrelated concepts. Are modules and typeclasses useful for this problem? What would be the recommended approach?

Answer 1

Indeed typeclasses were designed for this exact task, but then you face the hard problem of designing the particular class hierarchy that will fit your problem well.

Coq doesn't provide a standard hierarchy of mathematical operators, and there are many delicate trade-offs in building one with regard to the choice of classes, operators, and axioms.

I thus recommend starting from a mature development such as the MathComp library. MathComp is based on "Canonical Structures" which are a similar notion to type classes, and provides quite a few ready to use classes. The Packaging Mathematical Structures" paper contains more details, but the basic idea is that types pack their operators. For example, if you want to reason about abelian modules you can use the zmodType structure:

From mathcomp Require Import all_ssreflect all_algebra.

Open Scope ring_scope.
Definition sum (A: zmodType) (s : seq A) := foldr +%R 0 s.

to define the sum over a list of elements of the abelian group A. Even better, don't define you own sum operator and just use the one provided by the library: \sum_(x <- s) x:

Lemma eq_sum (A: zmodType) (s : seq A) : sum s = \sum_(x <- s) x.
Proof. by rewrite unlock. Qed.