Zulip Chat Archive

Stream: general

Topic: typeclasses considered harmful?

Huỳnh Trần Khanh (Dec 01 2021 at 06:11):

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 (Dec 01 2021 at 06:12):

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

Chris B (Dec 01 2021 at 06:21):

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

Kyle Miller (Dec 01 2021 at 06:35):

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 (Dec 01 2021 at 06:45):

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 (Dec 01 2021 at 06:45):

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

Stuart Presnell (Dec 01 2021 at 09:20):

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 (Dec 01 2021 at 09:21):

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

Johan Commelin (Dec 01 2021 at 09:21):

That's a typical example of how a diamond manifests

Alex J. Best (Dec 01 2021 at 09:23):

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 (Dec 01 2021 at 09:24):

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 (Dec 01 2021 at 09:38):


Last updated: Dec 20 2023 at 11:08 UTC