4
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ I'm not familiar enough with lean to answer but I think it's worth noting that in HoTT structures are implemented as dependent sum types, for example the type of magmas is $\sum_{A:\mathcal U}A\to A\to A$ while the type of semigroups is $\sum_{A:\mathcal U}\sum_{m:A\to A\to A}\prod_{x,y,z:A}m(x,m(y,z))=_A m(m(x,y),z)$, more axioms can be added similarly $\endgroup$ – Alessandro Codenotti Jul 6 at 11:53
  • $\begingroup$ @alessandroCodenotti, I dont fully underatand that notation but in Lean, a "structure" (as in, the keyword) generates pretty much a dependent sum type. Which is why I'm surprised that people dont use this, but instead use typeclasses. $\endgroup$ – user56834 Jul 6 at 13:45
  • $\begingroup$ In my previous comment I was using "structure" as "mathematical structure" rather than a formal term. It's quite awkward to phrase the assertion "a semigroup is a magma such that blabla" using only dependent sum types, while it's very clear while instantiating typeclasses though $\endgroup$ – Alessandro Codenotti Jul 6 at 13:48
  • $\begingroup$ There is a tag for LEAN on StackOverflow. $\endgroup$ – Derek Elkins Jul 6 at 22:28
  • $\begingroup$ @user56834 If you have further questions I recommend heading over to Zulip where it is easier to continue the conversation $\endgroup$ – Bruno Bentzen Jul 9 at 22:08
3
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ This clarifies! Question: Why don’t we use subtyping instead of typeclasses to achieve the same ends? E.g. have “commutative group” be a subtype of “group”. $\endgroup$ – user56834 Jul 7 at 9:25
  • 1
    $\begingroup$ Adding subtyping to a type system tends to utterly destroy various desirable properties. For example, type checking for even non-dependently typed languages with subtyping is often undecidable. This would be a huge problem for intensional type theories like Agda, Coq, and LEAN. NuPRL, an extensional type theory, does effectively have subtyping, but that's possible because equality reflection already gives up on decidable type checking and thus you provide typing derivations and not just types. This is a very different experience and view on types. $\endgroup$ – Derek Elkins Jul 7 at 10:09
  • 1
    $\begingroup$ Does it make sense to think of “typeclasses as applied to formalizing math” as basically “conceptually like subtyping but without the negative type-theoretic consequences”? $\endgroup$ – user56834 Jul 7 at 13:38
  • 1
    $\begingroup$ While type classes can be used to accomplish some of the some goals as subtyping, it doesn't make sense to pretend that they are something they're not. They work in a very different ways, and thus can be used to do different things. What makes sense is to understand what type classes are on their own terms. Here, it is better to (ahistorically) read the word "class" in the logical/set-theoretic way. A type class is a predicate on types. A type satisfying a particular such predicate implies that certain terms (constructively) exist. We can then talk about implications between these predicates. $\endgroup$ – Derek Elkins Jul 7 at 19:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.