typeclasses considered harmful?

Stream: general

[Huỳnh Trần Khanh]

hmm they're used extensively in mathlib... but I heard that if I use typeclasses a lot I will get... diamonds? well color me clueless I haven't used typeclasses before even though I know the syntax... hmm so what are diamonds? are they dangerous? how can I avoid them?

[Huỳnh Trần Khanh]

in rust there are traits, they are similar to typeclasses in many ways but diamonds don't exist in rust

[Chris B]

There's a description of "the diamond problem" with an example on page 5: https://arxiv.org/abs/2001.04301

[Kyle Miller]

I'm not sure if it's mentioned in that paper, but another flavor of the diamond problem is when through diamond inheritance you get conflicting definitions for things -- a subtle problem that affects theorem proving in contrast to normal software development is that the conflicting definitions might be equal but not definitionally equal.

I'm half-remembering a case involving algebraic structures and the natural numbers where the two operations were equal, but one inducted on the left argument and the other on the right. Edit: I think it was this: https://github.com/leanprover-community/mathlib/commit/63801552184f2a519c95a45561300547837915cc

[Chris B]

That's a good point. In Rust you can only have one implementation of a trait for a given type, so it doesn't matter which path you chase to get to the bottom of what looks like a diamond (I'm sure there's a counter-example for some unsafe box dyn &&*FnOnce something or other).

[Johan Commelin]

Does glossary#diamond work? [edit: yes it does :octopus:]

[Stuart Presnell]

So when someone reports that they have found a diamond, how does that manifest? Something running much more slowly than it should? Or Lean thinking there's a mismatch between things that appear to be identical?

[Johan Commelin]

You will get goals of the form foo = foo that aren't provable by rfl.

[Johan Commelin]

That's a typical example of how a diamond manifests

[Alex J. Best]

Because secretly under the hood the goal is something like @foo (bar.to_baz _inst_1) = @foo (quux.to_baz (bar.to_quux _inst_1)) and the two ways of getting baz from bar aren't definitionally equal.

[Stuart Presnell]

In the past I've seen Lean complain that some function expected argument x but was provided x (for some expression x). Might that be a result of a diamond?

[Kevin Buzzard]

Possibly