Classes vs Structures

Stream: new members

[Yasmine Sharoda]

Hello,
I am interested to know the reason why in Mathlib monoid is defined as a class, while monoid_hom is defined as a structure. What do we miss if we define both as classes or structures?
Also when projecting the member op of a class monoid, one need to qualify it as:

@monoid_class.op a m x1 x2

while projecting from a structure monoid can be sugared as

m.op_struc x1 x2

[Kevin Buzzard]

Mathematically, if you have a type M then probably you only want to consider one monoid structure on it. But if you have two monoids M and N, you might want to consider many monoid homomorphisms between them.

[Kevin Buzzard]

Class instances are automatically filled in by the type class inference system, which works under a "there is at most one term of this type" assumption.

[Kevin Buzzard]

so monoid_hom definitely shouldn't be a class, but there is no harm in making monoid a class.

[Eric Wieser]

Note that docs#is_monoid_hom is the class version of monoid_hom, but it was considered a failed design because simp was not able to use it

[Yasmine Sharoda]

Kevin Buzzard said:

Mathematically, if you have a type M then probably you only want to consider one monoid structure on it. But if you have two monoids M and N, you might want to consider many monoid homomorphisms between them.

But one might want to define on nat a monoid(nat,+,0,..) and monoid(nat,*,1,..)

[Eric Wieser]

In practice, mathlib does that by add_monoid(nat,+,0,..), which obviously doesn't scale to other monoid structures

[Adam Topaz]

This is more of an issue about morphisms and the distinction between (+) and (*).

[Kyle Miller]

A feature that class provides is that, for example, every group is automatically a monoid, so you can apply theorems about monoids to groups without any fuss. There isn't quite so deep of a hierarchy for homomorphisms, so this kind of automatic casting seems like it would be less beneficial.

What appears to be a plausible design heuristic for classes vs structures is whether you plan to do rewrites of terms. "Bundling" a term with its properties (like with monoid_hom) lets you rewrite that whole object while maintaining its properties, but if it were a class you'd have to worry about whether the associated typeclass still applies to the rewritten term. I think it's a lot less frequent rewriting an expression involving the monoid's type itself in comparison to rewriting expressions of homomorphisms. (If you work with finite sets, you can feel some of this with finset vs a set with a fintype instance.)

If I understand correctly, Coq uses structures for its algebraic hierarchy, but they use a feature called unification hints to do the automatic casting.

[Kevin Buzzard]

@Yasmine Sharoda it's what looks like an extraordinary design decision that Lean's monoids are bound to the notation * and we have a different but isomorphic class add_monoid bound to the notation +. I've never seen this approach in any other theorem prover. A lot of people are surprised by this! But we have a to_additive machine which duplicates all the lemmas for us automatically (so only one of the two needs to be stated, the multiplicative one) and it works just fine! So we have two classes, monoid and add_monoid, and we can have precisely one of each structure on a type with no trouble.

[Yasmine Sharoda]

Kyle Miller said:

A feature that class provides is that, for example, every group is automatically a monoid, so you can apply theorems about monoids to groups without any fuss. There isn't quite so deep of a hierarchy for homomorphisms, so this kind of automatic casting seems like it would be less beneficial.

What appears to be a plausible design heuristic for classes vs structures is whether you plan to do rewrites of terms. "Bundling" a term with its properties (like with monoid_hom) lets you rewrite that whole object while maintaining its properties, but if it were a class you'd have to worry about whether the associated typeclass still applies to the rewritten term. I think it's a lot less frequent rewriting an expression involving the monoid's type itself in comparison to rewriting expressions of homomorphisms. (If you work with finite sets, you can feel some of this with finset vs a set with a fintype instance.)

If I understand correctly, Coq uses structures for its algebraic hierarchy, but they use a feature called unification hints to do the automatic casting.

@Kyle Miller Can you please elaborate more on what you mean by "rewrites of terms"? Do you mean the terms of monoid language? and what does that have to do with bundling?

[Yasmine Sharoda]

Kevin Buzzard said:

Yasmine Sharoda it's what looks like an extraordinary design decision that Lean's monoids are bound to the notation * and we have a different but isomorphic class add_monoid bound to the notation +. I've never seen this approach in any other theorem prover. A lot of people are surprised by this! But we have a to_additive machine which duplicates all the lemmas for us automatically (so only one of the two needs to be stated, the multiplicative one) and it works just fine! So we have two classes, monoid and add_monoid, and we can have precisely one of each structure on a type with no trouble.

I understand that design decision. The automation provided by to_additive and other meta programs is what distinguishes Mathlib in a really good way. What I am asking is more of having a class like this one

class monoid_class (m : Type) : Type :=
  (e : m)
  (op : m -> m -> m)
  (assoc: ∀  x y z : m, op x (op y z) = op (op x y) z)
  (lunit : ∀ x : m, op e x = x)
  (runit : ∀ x : m, op x e = x)

and then creating 2 instances for nat, where you once instantiate op to be + and another time instantiate it to be *.
I am not sure if the two scenarios are the same of different!

[Kyle Miller]

With the monoid and monoid homomorphism examples, by rewriting terms I mean rewriting expressions involving monoids themselves or of monoid homomorphisms. For example, maybe you know that M = f M' and then rewrite according to this. Since you have [monoid M], you don't have [monoid (f M')] without rewriting the instance, too, so f M' isn't automatically a monoid itself.

[Eric Wieser]

Ultimately you have to hook into has_add, and I don't know how you'd do that with that example

[Kyle Miller]

The issue with your monoid_class is that you can't extend monoid_class twice

[Kyle Miller]

and op would be a name conflict

[Kyle Miller]

and also you're only supposed to have one instance of a class per set of indices, so you couldn't have nat be both a + monoid and a * monoid in a natural way. You'd want op to be one of the indices for the class for that, but then assoc and the rest would be name conflicts when you extend. If lean had some way to rename fields when extending, it might work.

[Yasmine Sharoda]

Kyle Miller said:

With the monoid and monoid homomorphism examples, by rewriting terms I mean rewriting expressions involving monoids themselves or of monoid homomorphisms. For example, maybe you know that M = f M' and then rewrite according to this. Since you have [monoid M], you don't have [monoid (f M')] without rewriting the instance, too, so f M' isn't automatically a monoid itself.

Thanks for the clarification.

[Yasmine Sharoda]

The second part of my question is why projecting a field of class monoid requires different syntax from projecting one from structure monoid.

• In the case of a class, one has to use @monoid_class.op a m x1 x2
• In the case of a structure, one can use m.op x1 x2 (where m is the name of the monoid instance)
  Is that just overlooking syntactic sugar? or is there a more profound reason?

[Kyle Miller]

If monoid_class is a structure, the type of op is

monoid_class.op : Π {m : Type}, monoid_class m → m → m → m

As a class, the type is

monoid_class.op : Π {m : Type} [c : monoid_class m], m → m → m

The difference between these is that class instance variable is automatically set to being inferred by the typeclass resolution system. This gives you the ability to write this:

open monoid_class (op)

example {m : Type*} [monoid_class m] (x y z : m) :
  op x (op y z) = op (op x y) z :=
monoid_class.assoc x y z

(The open line imports monoid_class.op into the current namespace, so you can write op for short.)

[Kyle Miller]

What you are observing is that @monoid_class.op changes the class instance argument to needing to be explicitly given. When all goes well, you don't need to pass class instance arguments.

[Kyle Miller]

When a class extends another, there is an automatically defined class instance definition. This lets you do the following:

class semigroup_class (m : Type) : Type :=
  (op : m -> m -> m)
  (assoc: ∀  x y z : m, op x (op y z) = op (op x y) z)

class monoid_class (m : Type) extends semigroup_class m : Type :=
  (e : m)
  (lunit : ∀ x : m, op e x = x)
  (runit : ∀ x : m, op x e = x)

open semigroup_class (op)

example {m : Type*} [monoid_class m] (x y z : m) :
  op x (op y z) = op (op x y) z :=
semigroup_class.assoc x y z

[Yasmine Sharoda]

Kyle Miller said:

What you are observing is that @monoid_class.op changes the class instance argument to needing to be explicitly given. When all goes well, you don't need to pass class instance arguments.

Thank you!