Zulip Chat Archive

Stream: general

Topic: Canonical structures


view this post on Zulip Kevin Sullivan (Oct 09 2018 at 16:31):

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.

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 16:36):

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?

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 16:39):

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

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 16:39):

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

view this post on Zulip Kevin Sullivan (Oct 09 2018 at 17:38):

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.

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 10:20):

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.

view this post on Zulip Patrick Massot (Oct 10 2018 at 11:05):

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.


Last updated: May 13 2021 at 18:26 UTC