Why does mathlib use typeclasses everywhere?

Stream: general

[Michael Jam]

Why does mathlib use typeclasses everywhere?
I'm looking at mathlib seriously for the first time and have odd feelings about the design. There's probably a whole history behind it that I can't really figure out..
If I had to do design a math library myself, I would probably start by not using typeclasses at all. I would use only structures and functions because its so easy to think with just them.
I think typeclasses make sense in software programming contexts, where you start by modeling requirements at high level using abstract types, and you can decide later what implementation you want to plug in or out. Now it's not obvious to me why they are so useful in a proof library. I think you'd want to have a unique canonical representation for a given math concept, and some functions/theorems directly defined on it. I'm not sure why you want to abstract behavior so much.
I have the impression that the main point of typeclasses in mathlib is to make some parameters and conversions implicit in order to make the code shorter. Mathlib design seems to assume that if it's shorter to write, it must be more simple. But is it really simpler to make information implicit if it becomes a hard problem to reconstruct it?
I feel like there is too much effort in making things look extremely short often to the detriment of readability. On the one hand, tactics are really great because they automate work that's hard to do by hand, and it's usually clear what they do. On the other hand, typeclasses remove some boilerplate that would be easy to write by hand, but now it's hard to understand what instance is used where.
I might sound crazy but I think I'd prefer converting inputs and passing instances explicitly every time i call a lemma in a proof. It's really a one time job, unlike in software programming where client requirements move all the time.
When I glance at the chat discussions, and papers about lean, there seems to have been a lot of effort spent on performance problems with instance resolution, with unintended diamonds and cycles, with design choices about bundled definitions, about the hierarchy... Surely I can find a lot about why typeclasses are causing problems, but actually I can't find much about why having them is so great/why not having them is so bad.
Now i'm certainly inexperienced and ignorant of all the history, I'm just throwing naive random thoughts as a newcomer. Were there past attempts at designing a mathlib without typeclasses? Are there papers/historical discussions/ list of examples on the usefulness of typeclasses in proof libraries?

[Johan Commelin]

@Michael Jam If I have a field $K$, and I want to apply a lemma to it about (additive) groups, then Lean can automatically figure out that $K$ is also an additive group. Thanks to typeclasses.
I'm very happy that I don't have to remind it of that fact all the time. And I'm also happy that I don't have to reprove every lemma for groups also for rings, commutative rings, division rings, fields, etc...

[Michael Jam]

yes well it's what I have a hard time being convinced of... I have the feeling you pay a high price for using them. I don't think I'd mind writing a function to convert a structure to another and adding them lazily as needed.

[Patrick Massot]

Michael, you get a very biased view by only reading messages here. People talk about instance searches here only when they encounter issues. But this hiding millions of uses where everything works perfectly smoothly. The overall outcome is this system works incredibly well.

[Patrick Massot]

And no major formalized math library operates without an analogous system (there are technical differences, but they are irrelevant to this conversation).

[Patrick Massot]

I don't know how to say it without sounding rude, so apologize in advance, but I think you're underestimating the complexity of mathematics. Carrying around explicit arguments would be a nightmare. Maybe Mario can do it in metamath, but that doesn't prove anything, and the goal of our work is not to make sure only Mario can use a proof assistant.

[Michael Jam]

Yes I understand. People write a lot more about what they have to complain about, than about what they are happy with. But I wonder if it's really that much an advantage to not convert structures explicitly. Do you spend that big of a fraction of your time using lean, calling different lemmas on different representations of a same structure?

[Patrick Massot]

I also think you spend way too much time trying to map what you understand from Haskell and programming in in general to theorem proving. I fear your messages don't make any sense because of this discrepancy.

[Michael Jam]

Yes I talk with zero experience, so I might be very wrong. I'm just curious in case you have more explicit or quantitative arguments. I know I'm gonna attract a lot of negative comments, but its a fast way to learn

[Patrick Massot]

Zero experience would probably easier actually. You seem to have experience with other things that bias your view in the wrong direction.

[Patrick Massot]

And I think trying to use Lean and mathlib the way it's written would be a faster way to learn than writing long messages that may sound like you wonder why people here are so stupid.

[Patrick Massot]

(Although I'm very ready to believe this is not what you mean)

[Michael Jam]

I'm very interested in Lean. Unfortunately I can't deep dive in it before the summer. I like socratic questioning. But i guess it often sounds like socratic irony... It's probably too early for me to ask questions then

[Yaël Dillies]

Just wanted to point out that writing proofs is most definitely not a one-time job. You reuse stuff everywhere, all the time. People push mathlib in all directions and we are very happy when we don't have to deal with the implicit lower level maths.

[Jannis Limperg]

I think it's just a question of scale. Explicit dictionary passing works okay -- perhaps better in some ways -- for small examples, but it becomes a huge PITA if you're working with bigger class hierarchies. Same for tactics versus proof terms. And scale issues are almost impossible to appreciate without experience because we always tend to think in small examples.

[Johan Commelin]

@Michael Jam How large do you think that the typeclass hierarchy of mathlib is? How many edges does that graph have? (I'm not even talking about the transitive closure. But if you chaining A -> B -> C -> D -> E explicitly is of course another big way to hamper readability.)

[Michael Jam]

I would write a function that does that chain once. And save it somewhere. I would not add all possible conversions, but I would add them lazily as needed over time

[Johan Commelin]

Sure, that's why I'm asking how many actual edges you think there currently are. (Not the transitive closure. But I'm warning that the number of edges is a lower bound for what we actually need in practice.)

[Michael Jam]

Probably way too many, that's why i'm suggesting to add them lazily, but how many are actually used in proofs? It cannot be that much longer than the number of proofs, or is it?

[Johan Commelin]

How many proofs do you think there are in mathlib :shock:

[Michael Jam]

probably a huge number... If you write a proof does it take a big fraction of your time writing the proof to add those conversions? if not already existing

[Johan Commelin]

We currently have 54576 theorems in mathlib and a bit more than 6000 instances.

[Johan Commelin]

Adding those explicit conversions would impact readability of statements (and proofs) massively. Lots of statements that now show the essence of the theorem in 1 line, would suddenly become several lines long, and hide the essence somewhere in the middle.

[Johan Commelin]

Proofs would become a lot more painful.

[Johan Commelin]

Anyway, I think the best way to find out that you replicate mathlibs algebraic hierarchy in a way that doesn't use typeclasses.

[Michael Jam]

Yes later I want to try to make a small dissenting mathlib to see how it feels. I'm not completely convinced by my approach either, it would be an interesting experiment, if it wasn't done in that past.

[Johan Commelin]

No! You shouldn't make it small.

[Johan Commelin]

As Jannis pointed out, for small examples your approach works fine.

[Johan Commelin]

I would think you want a hierarchy with a couple of hundred non-trivial edges, at least.

[Johan Commelin]

The 6000 instances that I quoted above are ones that are not auto-generated.

[Johan Commelin]

In reality there are many more.

[Michael Jam]

I have the feeling conversions could be done more cleanly with where clauses. But where does not seem very flexible in lean currently

[Michael Jam]

Now that I think about it, perhaps the explicit style I'm suggesting could be automatically generated from the current math lib? It feels possible

[Johan Commelin]

It would be really great if there was a prolog-like database that knew about a whole bunch of such conversions, and a bit of automation that would query the prolog-like database to automatically chain them together, and construct those where clauses whenever needed.

[Michael Jam]

It would be nice to convert the whole mathlib to typeclass-less mathlibs in different styles manipulating the AST.

[Michael Jam]

just to see what we get

[Michael Jam]

I'm not sure about the prolog like database. It feels too much like typeclasses. I want to keep explicitness

[Oliver Nash]

I think it's great to ask questions like this (even though I am convinced typeclasses provide far, far more value than they cost). I think a cheap way to get some sense of what they're doing for us is just to use set_option pp.implicit true and look at the results.

[Oliver Nash]

To take a concrete example, I just randomly picked the file abel_ruffini.lean, inserted set_option pp.implicit true at the top of the file and navigated to this line in VS code.

[Oliver Nash]

This shows allows me to see what the hypothesis hq : is_solvable (q.map (algebra_map F p.splitting_field)).gal looks like with all the implicit parameters filled in. Here's what you get:

[Oliver Nash]

@is_solvable
  (@map F p.splitting_field
     (@comm_semiring.to_semiring F
        (@comm_ring.to_comm_semiring F (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1))))
     (@ring.to_semiring p.splitting_field
        (@division_ring.to_ring p.splitting_field
           (@field.to_division_ring p.splitting_field (@splitting_field.field F _inst_1 p))))
     (@algebra_map F p.splitting_field
        (@comm_ring.to_comm_semiring F (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
        (@ring.to_semiring p.splitting_field
           (@division_ring.to_ring p.splitting_field
              (@field.to_division_ring p.splitting_field (@splitting_field.field F _inst_1 p))))
        (@splitting_field.algebra F _inst_1 p))
     q).gal
  (@gal.group p.splitting_field (@splitting_field.field F _inst_1 p)
     (@map F p.splitting_field
        (@comm_semiring.to_semiring F
           (@comm_ring.to_comm_semiring F (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1))))
        (@ring.to_semiring p.splitting_field
           (@division_ring.to_ring p.splitting_field
              (@field.to_division_ring p.splitting_field (@splitting_field.field F _inst_1 p))))
        (@algebra_map F p.splitting_field
           (@comm_ring.to_comm_semiring F (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
           (@ring.to_semiring p.splitting_field
              (@division_ring.to_ring p.splitting_field
                 (@field.to_division_ring p.splitting_field (@splitting_field.field F _inst_1 p))))
           (@splitting_field.algebra F _inst_1 p))
        q))

[Oliver Nash]

Notwithstanding the fact that the formalisation of Abel-Ruffini is an absolutely amazing achievement, this is still very elementary mathematics and already look at how large the term with implicit parameters displayed is.

[Johan Commelin]

@Michael Jam Another reason why I think typeclasses are really great: they allow us to use the notation x + y in lots of different contexts. Whether x and y are integers, real numbers, elements of $\Z/37\Z$ or live in some abstract vector space.
I think this is very important.

[Mario Carneiro]

Johan Commelin said:

It would be really great if there was a prolog-like database that knew about a whole bunch of such conversions, and a bit of automation that would query the prolog-like database to automatically chain them together, and construct those where clauses whenever needed.

I see what you did there...

[Mario Carneiro]

Oliver Nash said:

Notwithstanding the fact that the formalisation of Abel-Ruffini is an absolutely amazing achievement, this is still very elementary mathematics and already look at how large the term with implicit parameters displayed is.

I have mixed feelings about arguments of this form. While it's true that if you look at the terms that lean produces using typeclass inference that it would be hell to write that yourself, this isn't really a fair comparison because in the alternate world you would have short names for the relevant transitive instances. As Patrick alluded to, Metamath does things a little bit differently, and it basically boils down to having shortcut instances for common paths and using the lemma once per proof. When proofs are long this is a reasonable option since it is a small fraction of the full proof, but it is not incompatible with a prolog like proof search for these lemmas.

[Mario Carneiro]

Ultimately, the reason lean and mathlib use typeclasses so extensively is because lean was literally designed to use typeclasses as the hammer to solve every problem. It has a huge home field advantage compared to alternatives that are more verbose and less automatic.

[Joe Hendrix]

I'm not sure I know of a language that does this, but it might be interesting to explore resolving typeclasses by using a distance metric rather than priorities. The idea would be rather than requiring programmers to pick a priority for the class (and higher priorities are chosen first), you assign a cost to using the class. This would encourage the solver to take advantage of instances that provide path compression without requiring users to explicitly assign a global priority to each instance.

[Johan Commelin]

Ooh, that sounds quite interesting. Using Dijkstra on the hierarchy (-;