Why typeclasses rather than inductive types to define mathematical structures in Lean?

Question

I am not sure whether this is the right forum for this question, but I am not sure where else to ask (There is no Lean forum afaik).

In the Lean Prover mathlib library, typical mathematical structures such as groups, are formalized as “typeclasses”.

However, in the Lean prover online guide, I think the first mathematical structure defined is a Semigroup, which is defined as a “structure” (which if I understand correctly, is syntactic sugar for an inductive type). It seems sensible to me to formalize mathematical structures this way, since the Lean keyword “structure” essentially creates a cartesian product between types, which is exactly how mathematical structures are thought of: as tuples of data. (In fact, as a side question, this makes me wonder why we formalize them as structures at all, instead of just basic cartesian products, which are also defined in Lean).

So why do people formalize mathematical structures as type classes, instead of as products of types (i.e. as “structures” or “product types”), since the latter is quite close to the standard way of thinking about structures in mathematics?

Answer 1

Formalizing mathematics in a proof assistant involves what are essentially software engineering concerns that largely don't exist in informal mathematics.

Do you want to refer to G.commutative_law or G.2.1? Do you want error messages that say "Group does not match Setoid" or "sigma.mk S b does not match sigma.mk (S -> S -> Type) c? Do you want to edit all your proofs because you decided to rearrange the order of the laws?

These are the kinds of things that using a structure as opposed to tuples would address.

Do you want to have to explicitly show that each property you prove about all groups also applies to commutative groups? Do you want to constantly convert between representations to apply different proofs, e.g. viewing a semi-lattice as a monoid? Do you want to build a structure witnessing that some particular type is a monoid and another to witness that it is a group and another to witness that it is a ring, or would you rather just assert laws and operators and have this be inferred? Do you want to explicitly construct the ring of matrices whose components are polynomials whose coefficients are rationals, or would you want this automatically constructed from general results?

These are the kinds of things that using type classes as opposed to structures would address.

This is not to say that there are no trade-offs, and there aren't arguments to do things different ways. There are many ways to approach designing mathematical libraries and what you consider important will dictate the design that makes sense.

The software engineering concerns are things like:

• Modularity — changes inside of one component don't require changes elsewhere
• Information hiding — using a matrix of integers should be as easy as using a matrix of polynomials with coefficients in real functions
• Extensibility — it should be easy to reuse an existing definition to make a more elaborate one, e.g. we should be able to reuse the definition of groups in the definition of rings
• Ease of use — we should be able to express things in a natural way without a lot of boilerplate or clutter
• Performance — yes, this matters for proof assistants, you don't want it to take 10 minutes every time you load a file

One goal of proof assistants is to get as close as possible to how mathematicians write math, not the halfhearted attempt to add a touch of "formality". Mathematicians may say something like, "a group is a tuple $(S,1,(-)^{-1},\cdot)$" but they certainly don't then go on to write, "let $G$ be a group, then $x\mapsto\pi_4(G)(x,\pi_3(G)(x))=x\mapsto\pi_2(G)$ as functions on $\pi_1(G)$."

A major component that informal definitions and proofs omit is what programmers call "glue code". Formally, this can't be omitted; however, by carefully designing your definitions it can be reduced. This takes a good amount of skill to do well. Language features can provide more tools to achieve this or offload the work onto the language so it doesn't clutter up what's written.

You can, if you want, do things in Lean more like mathematicians nominally appear to formalize things. You will quickly find that it is extremely unpleasant and tedious to work with and produces incomprehensible code if a lot of work isn't put in to avoid it.

I suspect many (though still a small minority) of mathematicians have attempted to be "fully rigorous" and been turned off by the large amount of seemingly inane detail that arises. They don't realize that they are using inappropriate tools and working with definitions that were meant to show a construction is possible with minimal requirements and were not made with any thought toward usability. For example, a slight improvement over the group example before would be to define a group as a function on $\{\mathsf{carrier},\mathsf{unit},\mathsf{inverse},\mathsf{mult}\}$ and the equation from before would become $x\mapsto G(\mathsf{mult})(x,G(\mathsf{inverse})(x))=x\mapsto G(\mathsf{unit})$ which is still not great but is at least comprehensible.