A compendium of WhatNotToDo

[JacquesCarette]

(as suggested by @jamesmckinna in a comment in #3053).

Each subsequent post should be an example of design that turns out to be... sub-optimal. Negative examples are also quite informative.

[JacquesCarette]

Example 1: Lean's AdditiveMonoid and MultiplicativeMonoid.

Obviously, there is no such thing. The "reason" for the design is purely one of notation, and a system weakness where 'renaming' is not a first-class operation in Lean.

[JacquesCarette]

Example 2: Over-reliance of 'CanonicalStructures' in Rocq.

This is a particular case of unbundling, coupled with a very special case of typeclasses. The latter conflates two ideas: interfaces and dynamic dispatch. CanonicalStructures are single-parameter typeclasses with the 'carrier set' (a la Pebble) in focus.

There is a bad habit amongst mathematicians to use the same name for a structure (like the ring of integers) and its carrier set. This has pushed system builders to try to create features that emulate this overloading. It would be good to document the myriad ways in which this is a bad idea. But we can start by naming it as such.

[JacquesCarette]

Example 3: no support for diamonds.

I think Isabelle locales are the "least weak" here, but basically all systems believe that 'theory hierarchies' are exactly that, hierarchies. They are not, they are quite full of 'diamonds'. And, unlike the same shape for implementation inheritance where such diamonds are evil, in signatures, they are quite tame. Useful. The ML-family's post-facto where to merge signatures is a giant hack that lets one deal with some diamonds, but it does not scale well.