Canonical structures

Stream: general

[Kevin Sullivan]

Will there be, or is there, an analog of Coq's "canonical structures", complementary to typeclasses, in Lean?

For information about canonical structures, see Canonical Structures for the working Coq user, https://hal.inria.fr/hal-00816703v2, Sandrine Blazy and Christine Paulin and David Pichardie. ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.19-34, 2013, LNCS. 〈10.1007/978-3-642-39634-2_5.

[Kevin Buzzard]

I've heard these things mentioned here in the past, and my impression is that at least some people seem to think that Lean's typeclasses are "better". Am I completely wrong about this?

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/working.20with.20finite.20sequences/near/123573886

[Kevin Buzzard]

Some old discussion on the same topic. If you have things to add I'm sure that people here would be interested.

[Kevin Sullivan]

Some old discussion on the same topic. If you have things to add I'm sure that people here would be interested.

Ah, thanks for the link to this thread. I did a search before posting but didn't come up with this one.

[Kevin Buzzard]

I found it using search -- searching for canonical structures gave me a bunch of posts by me banging on about canonical isomorphisms of structures; I then realised that searching for "canonical structure" was a better idea.

[Patrick Massot]

About canonical structures, the only interesting thing I remember is that, in the Coq bigop paper, they insist a lot on the fact that canonical structures can be associated to terms and not only types, and this is meant to be a huge advantage over type classes. But this does not apply to Lean type classes. For instance the is_commutative type class in https://github.com/leanprover/lean/blob/ceacfa7445953cbc8860ddabc55407430a9ca5c3/library/init/algebra/classes.lean#L13 is about a term.