Typeclasses for morphisms

Stream: general

[Eric Wieser]

I've been finding bundled morphisms very irritating to write lemmas about. Consider:

-- the actual lemma
lemma zero_hom.map_single_apply {α : Type*} {β : Type*} {γ : Type*} [has_zero β] [has_zero γ] (i j : α)
(v : β) (f : zero_hom β γ) :
  f (finsupp.single j v i) = finsupp.single j (f v) i :=
by rw [finsupp.single_apply, finsupp.single_apply, apply_ite f, f.map_zero]

-- the tedious copy paste operation
lemma add_monoid_hom.map_single_apply {α : Type*} {β : Type*} {γ : Type*} [add_monoid β] [add_monoid γ] (i j : α)
(v : β) (f : β →+ γ) :
  f (finsupp.single j v i) = finsupp.single j (f v) i :=
f.to_zero_hom.map_single_apply _ _ _
lemma ring_hom.map_single_apply {α : Type*} {β : Type*} {γ : Type*} [semiring β] [semiring γ] (i j : α)
(v : β) (f : β →+* γ) :
  f (finsupp.single j v i) = finsupp.single j (f v) i :=
f.to_add_monoid_hom.map_single_apply _ _ _
lemma alg_hom.map_single_apply {α : Type*} {β : Type*} {γ : Type*} [semiring β] [semiring γ] [algebra R β] [algebra R γ] (i j : α)
(v : β) (f : β →ₐ[R] γ) :
  f (finsupp.single j v i) = finsupp.single j (f v) i :=
f.to_ring_hom.map_single_apply _ _ _

While I only have to write an interesting proof once, I'm then forced to manually copy across the lemma to every single derived hom structure if I want it to be useful - something that wouldn't be necessary if type class inference were involved.

[Yury G. Kudryashov]

Earlier we migrated from the typeclass approach because Lean can't effectively use is_add_monoid_hom.map_add as a simp lemma.

[Yury G. Kudryashov]

Clearly, we need more automation here but I don't know how to implement it (read: my meta programming skills are not good enough for the job).

[Reid Barton]

I think there was a suggestion at one point that if structure B extends A and f : B and there is A.foo but no B.foo then f.foo means f.to_A.foo.

[Reid Barton]

I don't know if this is something planned for Lean 4 though.

[Reid Barton]

also, I guess there might be minor details which this doesn't address, e.g. the lemma add_monoid_hom.map_single_apply above is stated in terms of add_monoid_hom's coercion to function but its definition would be stated in terms of zero_hom's coercion to function

[Yury G. Kudryashov]

We also need to automatically make (f : ring_hom).to_monoid_hom.map_mul it a simp lemma. I think, it should be easier to have a command "import the following lemmas using this projection".

[Yury G. Kudryashov]

Or "import all lemmas about f.to_monoid_hom marked with an attribute"

[Yury G. Kudryashov]

The command should be clever enough to replace [monoid M] with [ring R] and [comm_monoid M] with [comm_ring R].

[Eric Wieser]

Relatedly I'd like to be able to write rw monoid_hom.map_mul and have it match ring_hom too

[Kevin Buzzard]

That's funny, I never rewrite stuff like that -- I always rewrite stuff like f.map_mul (so basically it's guaranteed to use the right one)

[Eric Wieser]

I suppose my actual case was where I just wanted to do all of them in a simp_rw

[Adam Topaz]

I think it's also useful when you have some structure extending, say, a monoid_hom.

[Adam Topaz]

It's annoying to write f.to_monoid_hom.map_mul or whatever

[Eric Wieser]

Right, but that has the same solution as the original problem

[Chris Hughes]

Kevin Buzzard said:

That's funny, I never rewrite stuff like that -- I always rewrite stuff like f.map_mul (so basically it's guaranteed to use the right one)

Trouble with this is sometimes f is really long

[Eric Wieser]

Yury G. Kudryashov said:

Earlier we migrated from the typeclass approach because Lean can't effectively use is_add_monoid_hom.map_add as a simp lemma.

Can you elaborate a bit on why that's true? Why can lean use things like inv_inv as simp lemmas, which also depend on typeclass resolution?
Is the issue has_coe_to_fun?

[Yury G. Kudryashov]

docs#is_add_monoid_hom.map_add has no coe_fn in it. OTOH, docs#add_monoid_hom.map_add has @coe_fn (add_monoid_hom), and simp can match on it.

[Yury G. Kudryashov]

Similarly, simp can match has_inv.inv in inv_inv, then start searching for the instance.

[Eric Wieser]

But simp can't match [is_add_monoid_hom f] in is_add_monoid_hom.map_add?

[Yury G. Kudryashov]

It looks at my_fun (a + b). It doesn't know that my_fun is a homomorphism at this moment.

[Eric Wieser]

My thinking was that it would match against the lemma statement of is_add_monoid_hom.map_add as its statement matches f (a + b), then find the predicate [is_add_monoid_hom f] as the second step. Is that not how simp matching works?

[Yury G. Kudryashov]

simp works well if it can match on the head symbol.

[Anne Baanen]

@Eric Wieser encountered an instance where the unbundled type classes make sense. Consider:

@[simp] lemma matrix.is_zero_hom_map_zero
  {α β : Type*} [has_zero α] [has_zero β] (f : α -> β) [is_zero_hom f] :
  (0 : matrix n n α).map f = 0 := sorry

Since the head symbol is matrix.map, this is a useful simp lemma, correct? The current is_foo_hom typeclasses do not have instances (f : foo_hom) : is_foo_hom f, unfortunately, so we cannot use the unbundled predicate yet. The alternative would be to copy the declaration for each foo_hom, which doesn't sound very scalable.

So here is my modest proposal for uniting the unbundled and bundled dichotomy:

• create an is_foo_hom typeclass for each foo_hom that doesn't have one yet
• add instance (f : foo_hom) : is_foo_hom f and nothing more, except:
• whenever bar_hom extends foo_hom, is_bar_hom should extend is_foo_hom
• instead of defining @[simp] lemma foo_hom.map_qux (f : foo_hom) : coe_fn f qux = quux, define @[simp] lemma is_foo_hom.map_qux {foo_hom_like : Type*} (f : foo_hom_like) [is_foo_hom f] : coe_fn f qux = quux.

Thoughts?

[Eric Wieser]

I don't understand your last bullet point - the lemma involves the derived structure bar_hom, which surely results in the same duplication we're trying to avoid?

[Anne Baanen]

Ah, the trick is the {bar_hom : Type*} parameter: for any type whose inhabitants are foo_homs, we have the lemma. I see how the name is confusing, let me rephrase it...

[Eric Wieser]

"if bar_hom extends foo_hom" - is this solved by just having is_bar_hom extend is_foo_hom?

[Anne Baanen]

You're right :face_palm:

[Eric Wieser]

So would the rule become "inputs should use typeclass homs, outputs bundled homs", or is it more subtle?

[Anne Baanen]

That sounds like a good rule of thumb, maybe qualified with "an input f should be an unbundled hom if it does not appear as a head symbol"? Or just arrange things so that they don't appear in that position?

[Anne Baanen]

Perhaps lift-like operations need to stay bundled to ensure coherence? I don't know.

[Sebastien Gouezel]

Wouldn't it be nicer to have some kind of tactic framework if we have bundled definitions that all satisfy the same kind of properties, to generate all the basic lemmas for the structure? For instance, there are many equiv-like structures. If we could tag them with @equiv, it could generate things like apply_symm_apply and the likes (currently, I see 9 instances of Lemma/Theorem apply_symm_apply in mathlib, for 9 different equiv-like structures). I have the impression that your problem belongs to the same kind of question: a framework to generate a basic skeleton that comes again and again.

[Sebastien Gouezel]

(I should say that I am not over-enthusiastic over the idea to rely again on non-bundled stuff, because for me the move to bundled stuff made things really better. But if you find a nice way to solve your problem using them, and if this could scale to equivs and the likes, maybe it just means that your way of using them is just more clever than what we did before!)

[Eric Wieser]

"as a head symbol" means "not coe_fun f arg? Is f even the head symbol there anyway?

[Anne Baanen]

If generating lemmas with tactics works well (and I don't have to write it), I'm also for it. Although it feels like we're working against Lean to get what we want, instead of using typeclasses for what they were intended.

[Eric Wieser]

Does the whole head symbol problem go away if we're using [is_hom f_type] instead of [is_hom f]?

[Anne Baanen]

Eric Wieser said:

"as a head symbol" means "not coe_fun f arg? Is f even the head symbol there anyway?

In that case, coe_fun is the head symbol. The reason for the qualification is that many tactics categorize lemmas based on the head symbol. So when simp traverses the subexpressions, it can do a quick equality-of-symbols check to see if this subexpression is relevant, rather than doing a big unification with each possible simp lemma. Similarly for library_search, etc.

[Anne Baanen]

So [is_zero_hom f] : f 0 = 0 is problematic, but [is_zero_hom (coe_fn f)] : coe_fn f 0 = 0 would work.

[Anne Baanen]

I have a meeting in a couple of minutes, in 90 minutes or so I can try writing a concrete example to see if this idea holds any water.

[Eric Wieser]

If f is not a function, then surely automatic coercion means it is never a head symbol, and the coercion is?

[Anne Baanen]

Right, but is_zero_hom would take f : α → β as an argument (it needs to since you can't easily get the domain/codomain from a general has_coe_to_fn instance). But then you'd be tempted to "generalize" is_zero_hom.map_zero to adding f : α → β as an argument to your lemma instead of f : is_foo_hom_like.

[Anne Baanen]

Bah, has_coe_to_fun as a typeclass argument doesn't work well at all:

variables {M N : Type*}

class is_zero_hom [has_zero M] [has_zero N] (f : M → N) :=
(map_zero' : f 0 = 0)

@[simp] lemma is_zero_hom.map_zero {zero_hom_like : Type*} [has_coe_to_fun zero_hom_like]
  (f : zero_hom_like) [is_zero_hom (coe_fn f)] : -- error: expected `? -> ?`, got `has_coe_to_fun.F f`
  f 0 = 0 :=
is_zero_hom.map_zero'

[Eric Wieser]

Can you make is_zero_hom extend has_coe_to_fun somehow?

[Eric Wieser]

Or use (f : M → N) instead of coe_fn f?

[Anne Baanen]

I'm trying something like the first option now:

class is_hom (hom M N : Type*) :=
(coe : hom → M → N)

variables {hom M N : Type*}

instance is_hom.to_coe_fn [is_hom hom M N] : has_coe_to_fun hom :=
{ F := λ _, M → N,
  coe := is_hom.coe }

class is_zero_hom [has_zero M] [has_zero N] [is_hom hom M N] (f : hom) :=
(map_zero : f 0 = 0)

[Anne Baanen]

But I suspect that M and N should be out_params for is_zero_hom

[Anne Baanen]

This seems to work:

import algebra.group.hom

/-

/-- Homomorphism that preserves zero -/
structure zero_hom (M : Type*) (N : Type*) [has_zero M] [has_zero N] :=
(to_fun : M → N)
(map_zero' : to_fun 0 = 0)

/-- Homomorphism that preserves addition -/
structure add_hom (M : Type*) (N : Type*) [has_add M] [has_add N] :=
(to_fun : M → N)
(map_add' : ∀ x y, to_fun (x + y) = to_fun x + to_fun y)

/-- Bundled add_monoid homomorphisms; use this for bundled add_group homomorphisms too. -/
structure add_monoid_hom (M : Type*) (N : Type*) [add_monoid M] [add_monoid N]
extends zero_hom M N, add_hom M N

-/

class is_hom_type (hom : Type*) (M N : out_param $ Type*) :=
(coe : hom → M → N)

variables {hom M N : Type*}

instance is_hom_type.to_coe_fn [is_hom_type hom M N] : has_coe_to_fun hom :=
{ F := λ _, M → N,
  coe := is_hom_type.coe }

class is_zero_hom {hom : Type*} {M N : out_param $ Type*}
  [has_zero M] [has_zero N] [is_hom_type hom M N] (f : hom) :=
(map_zero : f 0 = 0)

attribute [simp] is_zero_hom.map_zero

instance zero_hom.is_hom_type [has_zero M] [has_zero N] : is_hom_type (zero_hom M N) M N :=
⟨λ f, f⟩

instance zero_hom.is_zero_hom [has_zero M] [has_zero N] (f : zero_hom M N) :
  is_zero_hom f :=
⟨f.map_zero'⟩

class is_add_hom {hom : Type*} {M N : out_param $ Type*}
  [has_add M] [has_add N] [is_hom_type hom M N] (f : hom) :=
(map_add : ∀ x y, f (x + y) = f x + f y)

instance add_hom.is_hom [has_add M] [has_add N] : is_hom_type (add_hom M N) M N :=
⟨λ f, f⟩

instance add_hom.is_add_hom [has_add M] [has_add N] (f : add_hom M N) :
  is_add_hom f :=
⟨f.map_add'⟩

attribute [simp] is_add_hom.map_add

class is_add_monoid_hom [add_monoid M] [add_monoid N] [is_hom_type hom M N] (f : hom)
extends is_zero_hom f, is_add_hom f

instance add_monoid_hom.is_hom [add_monoid M] [add_monoid N] : is_hom_type (add_monoid_hom M N) M N :=
⟨λ f, f⟩

instance add_monoid_hom.is_add_monoid_hom [add_monoid M] [add_monoid N] (f : M →+ N) :
  is_add_monoid_hom f :=
{ map_zero := f.map_zero',
  map_add := f.map_add' }

section test

local attribute [-simp] add_zero add_hom.map_add add_monoid_hom.map_add add_monoid_hom.map_zero zero_hom.map_zero

example [add_monoid M] [add_monoid N] {f : M →+ N} {g : N →+ M} (x y : M) :
  g.comp f (x + y + 0) = g (f x + f y) + 0 := by squeeze_simp

end test

[Eric Wieser]

Having is_zero_hom extend is_hom didn't work?

[Anne Baanen]

The names are a bit confusing, but is_hom is a predicate on the type hom, while is_zero_hom is a predicate on an element f : hom. So extending is not what we want. I will rename is_hom -> is_hom_type.

[Eric Wieser]

while is_zero_hom is a predicate on an element f : hom.

Why is this better than having it be a predicate on hom itself?

[Eric Wieser]

That is,

class is_zero_hom {hom : Type*} {M N : out_param $ Type*}
[has_zero M] [has_zero N] [is_hom_type hom M N] :=
(map_zero : ∀ (f : hom), f 0 = 0)

[Anne Baanen]

I get an error:

class is_hom (hom : Type*) (M N : out_param $ Type*) :=
(coe : hom → M → N)

variables {hom M N : Type*}

instance is_hom.to_coe_fn [is_hom hom M N] : has_coe_to_fun hom :=
{ F := λ _, M → N,
  coe := is_hom.coe }

class is_zero_hom (hom : Type*) {M N : out_param $ Type*}
  [has_zero M] [has_zero N] extends is_hom hom M N :=
(map_zero : ∀ (f : hom), f 0 = 0)

class is_add_hom (hom : Type*) {M N : out_param $ Type*}
  [has_add M] [has_add N] extends is_hom hom M N :=
(map_add : ∀ (f : hom) x y, f (x + y) = f x + f y)

class is_add_monoid_hom (hom : Type*) {M N : out_param $ Type*} [add_monoid M] [add_monoid N]
extends is_zero_hom hom, is_add_hom hom -- don't know how to synthesize placeholder `(out_param Type*)`

[Anne Baanen]

Let's try making M and N explicit then...

[Anne Baanen]

Yup, that also works:

import algebra.group.hom

/-

/-- Homomorphism that preserves zero -/
structure zero_hom (M : Type*) (N : Type*) [has_zero M] [has_zero N] :=
(to_fun : M → N)
(map_zero' : to_fun 0 = 0)

/-- Homomorphism that preserves addition -/
structure add_hom (M : Type*) (N : Type*) [has_add M] [has_add N] :=
(to_fun : M → N)
(map_add' : ∀ x y, to_fun (x + y) = to_fun x + to_fun y)

/-- Bundled add_monoid homomorphisms; use this for bundled add_group homomorphisms too. -/
structure add_monoid_hom (M : Type*) (N : Type*) [add_monoid M] [add_monoid N]
extends zero_hom M N, add_hom M N

-/

set_option old_structure_cmd true

class is_hom (hom : Type*) (M N : out_param $ Type*) :=
(coe : hom → M → N)

variables {hom M N : Type*}

instance is_hom.to_coe_fn [is_hom hom M N] : has_coe_to_fun hom :=
{ F := λ _, M → N,
  coe := is_hom.coe }

class is_zero_hom (hom : Type*) (M N : out_param $ Type*)
  [has_zero M] [has_zero N] extends is_hom hom M N :=
(map_zero : ∀ (f : hom), f 0 = 0)

attribute [simp] is_zero_hom.map_zero

instance zero_hom.is_zero_hom [has_zero M] [has_zero N] : is_zero_hom (zero_hom M N) M N :=
{ coe := λ f, f.to_fun,
  map_zero := λ f, f.map_zero' }

class is_add_hom (hom : Type*) (M N : out_param $ Type*)
  [has_add M] [has_add N] extends is_hom hom M N :=
(map_add : ∀ (f : hom) x y, f (x + y) = f x + f y)

instance add_hom.is_add_hom [has_add M] [has_add N] :
  is_add_hom (add_hom M N) M N :=
{ coe := λ f, f.to_fun,
  map_add := λ f, f.map_add' }

attribute [simp] is_add_hom.map_add

class is_add_monoid_hom (hom : Type*) (M N : out_param $ Type*) [add_monoid M] [add_monoid N]
extends is_zero_hom hom M N, is_add_hom hom M N

instance add_monoid_hom.is_add_monoid_hom [add_monoid M] [add_monoid N] :
  is_add_monoid_hom (M →+ N) M N :=
{ coe := λ f, f.to_fun,
  map_zero := λ f, f.map_zero',
  map_add := λ f, f.map_add' }

section test

local attribute [-simp] add_zero add_hom.map_add add_monoid_hom.map_add add_monoid_hom.map_zero zero_hom.map_zero

example [add_monoid M] [add_monoid N] {f : M →+ N} {g : N →+ M} (x y : M) :
  g.comp f (x + y + 0) = g (f x + f y) + 0 := by squeeze_simp

end test

[Eric Wieser]

Is add_monoid_hom.is_hom needed there?

[Anne Baanen]

We can delete it, indeed.

[Eric Wieser]

And I suppose

example [add_monoid M] [add_monoid N] {hom1 : Type*} {hom2 : Type*}
  [is_add_monoid_hom hom1 M N]
  [is_add_monoid_hom hom2 N M] {f : hom1} {g : hom2} (x y : M) :
  g (f (x + y + 0)) = g (f x + f y) + 0 := by squeeze_simp

is how you'd write your example with the new typeclasses, so that it works "by magic" on ring_homs too

[Anne Baanen]

Indeed, something like that. I wanted to make sure that comp worked well which is why I included it. Since that was an important motivation to bundle homs (if I understand the history correctly).

[Eric Wieser]

Unfortunately that's rather hard to read snice the "type" of f and g is no longer inline

[Anne Baanen]

Maybe is_hom should include id, comp and ext, to look more like category_theory.bundled_hom:

structure bundled_hom :=
(to_fun : Π {α β : Type u} (Iα : c α) (Iβ : c β), hom Iα Iβ → α → β)
(id : Π {α : Type u} (I : c α), hom I I)
(comp : Π {α β γ : Type u} (Iα : c α) (Iβ : c β) (Iγ : c γ),
  hom Iβ Iγ → hom Iα Iβ → hom Iα Iγ)
(hom_ext : ∀ {α β : Type u} (Iα : c α) (Iβ : c β), function.injective (to_fun Iα Iβ) . obviously)
(id_to_fun : ∀ {α : Type u} (I : c α), to_fun I I (id I) = _root_.id . obviously)
(comp_to_fun : ∀ {α β γ : Type u} (Iα : c α) (Iβ : c β) (Iγ : c γ)
  (f : hom Iα Iβ) (g : hom Iβ Iγ),
  to_fun Iα Iγ (comp Iα Iβ Iγ g f) = (to_fun Iβ Iγ g) ∘ (to_fun Iα Iβ f) . obviously)

[Anne Baanen]

(Luckily we wouldn't have c : Type u → Type u forcing everything into the same universe!)

[Eric Wieser]

I just had a go at using something like class is_hom (hom : Type u₂ → Type u₃ → Type u₁), but I don't think it works out

[Anne Baanen]

You can't instantiate that kind of is_hom for zero_hom, since not all Type us have a zero :(

[Eric Wieser]

Exactly

[Eric Wieser]

docs#category_theory.bundled_hom since I'm lazy

[Eric Wieser]

I see the c α arguments end up holding the type-classes

[Eric Wieser]

I don't see how you can get comp in a structure in any sensible way - how do I write comp for (A → B) → (B → C) → (A → C) if all three types live in different universes? I'd need a universe quantifier in a field, which isn't allowed

[Eric Wieser]

Anne Baanen said:

(Luckily we wouldn't have c : Type u → Type u forcing everything into the same universe!)

That is, I don't see how you plan to lift the restriction you mention in this comment

[Anne Baanen]

You are correct, we cannot add a good definition for id or comp. ext works though:

class is_hom (hom : Type*) (M N : out_param $ Type*) :=
(coe : hom → M → N)
(ext : function.injective coe)

[Anne Baanen]

I guess we can have has_comp (homMN homNO : Type*) (homMO : out_param Type*) and has_id typeclasses with the coherence conditions in there, but that would be an inference disaster. :(

[Eric Wieser]

Related: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/universes/near/214217753

[Yury G. Kudryashov]

The main problem with "use coe_fn as the head symbol" trick is that docs#has_coe_to_fun does not allow us to require "type hom_type has coercion to M → N".

[Yury G. Kudryashov]

This happens because F is a part of the output, not an out_param

[Eric Wieser]

Is this something that lean4 could change the mechanics of, or would the out_param choice be worse in other ways?

[Anne Baanen]

The is_hom class is supposed to fix that issue by putting the requirement in there. The only drawback is that the has_coe_to_fun instance must derive from is_hom for simp to work correctly?

[Anne Baanen]

Or would there be another issue I'm missing?

[Kevin Buzzard]

In algebra also, the move to bundled homs has been very nice. I would like to challenge the idea that having about 10 map_zero lemmas "doesn't scale". I think it's scaling really nicely. It is linear in the number of interesting collections of bundled morphisms, and this collection is not going to grow too much bigger in the near future -- the algebraic hierarchy is not going to massively expand randomly because someone discovers a fundamental new class of objects like groups, rings etc. I'm not saying I'm against the idea of bringing back is_ring_hom but remember that the reason we removed it is that it doesn't work very well; Lean 3 didn't like it.

[Eric Wieser]

I think it's scaling really nicely. It is linear in the number of interesting collections of bundled morphisms

The problem is that it's bilinear (O(N*M)) not just O(N); it's also linear in the number of interesting things you can apply morphisms to - sums over finsets, sums over finsupp, mapping over a matrix, ... The github comment linked to in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Typeclasses.20for.20morphisms/near/215428568 gives an example of this.

[Anne Baanen]

I'm definitely not planning on replacing ring_hom with unbundled structures. If you like your bundled homs, you can keep them :)

[Anne Baanen]

Another way we can phrase is_ring_hom x without referring to unbundled stuff is "this type has a coherent definition of coe : x -> ring_hom".

[Mario Carneiro]

I am similarly opposed to using lots of unbundled hom classes. However, you can achieve the original goal without too much work: have an is_zero_hom f class, and instances (f : A ->*+ B) : is_zero_hom f and so on. There is no quadratic growth of lemmas that way

[Eric Wieser]

I think that's what @Anne Baanen's example above does?

[Mario Carneiro]

I see anne suggesting a lot more than that

[Eric Wieser]

Do you object to the contents of this message? https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Typeclasses.20for.20morphisms/near/215444243

[Mario Carneiro]

yes, I don't think this should be a generic is_hom

[Mario Carneiro]

this will make the typeclass problem a lot harder

[Eric Wieser]

is_hom is only there as a trick to make has_coe_to_fun happy, it's not intended as API I think

[Mario Carneiro]

it still interposes on the coe typeclass problem that we use everywhere

[Eric Wieser]

I'm not sure what you mean by that - is your claim that the existance of is_hom will break typeclass resolution somewhere else? Slow it down? Or something else?

[Mario Carneiro]

it will slow it down

[Eric Wieser]

Is the issue that all has_coe_to_fun lookup will try looking for is_hom instances?

[Mario Carneiro]

yes, as well as back chaining through is_zero_hom, is_add_hom and all the rest

[Eric Wieser]

But typeclass resolution already does this for things like has_add, right? Why are we concerned about reusing the same mechanism?

[Eric Wieser]

At risk of constructing a straw man, this sounds a bit like "I don't like the idea of monoid A because it will slow down type-class inference for has_mul A (by back-chaining through cancel_monoid, ring, ...)"

[Mario Carneiro]

This is an actual problem though, monoid -> has_mul is not exempt

[Mario Carneiro]

What I don't want is to open a whole new world of stuff for typeclass inference to explore

[Mario Carneiro]

so "foundational" typeclass instances like the is_hom -> has_coe_to_fun one here that have no content on their own can singlehandedly double the size of the search

[Mario Carneiro]

it would be nice if we had a performance monitor for typeclass searches, so we can quantify performance regressions

[Mario Carneiro]

I'm pretty sure it's responsible for half of mathlib's compile time (the other half being VM evaluation)

[Mario Carneiro]

My suggestion is the same as the first two points of Anne's first post, without the "except"

[Mario Carneiro]

with that approach you won't be searching for an is_zero_hom class unless you actually apply matrix.is_zero_hom_map_zero

[Mario Carneiro]

so it's not going to make things worse for an unrelated file

[Eric Wieser]

Mario Carneiro said:

My suggestion is the same as the first two points of Anne's first post, without the "except"

How would you define is_add_hom then?

[Mario Carneiro]

only if it comes up for something else

[Mario Carneiro]

and there would not be an instance [is_add_hom f] : is_zero_hom f

[Mario Carneiro]

this keeps the typeclass problem very local

[Eric Wieser]

So now I need a is_zero_hom instance for add_monoid_hom, ring_hom, algebra_hom, linear_map?

[Mario Carneiro]

yes

[Eric Wieser]

So the work is now quadratic in the depth of the hom heirarchy

[Mario Carneiro]

yes, it's quadratic in 5

[Eric Wieser]

Which I suppose is slightly better than the bilinear case we have now

[Mario Carneiro]

however, individual typeclass problems are only linear in 5

[Mario Carneiro]

honestly, if I could have direct instances A -> B for every pair of classes A and B in the hierarchy that would be far better than the current exponential situation

[Eric Wieser]

Why is the current situation exponential anyway?

[Mario Carneiro]

unfortunately the way lean 3 typeclass inference works adding those shortcut instances only raises the base of the exponential

[Eric Wieser]

If my heirarchy were a single branch of a tree, then surely a "get typeclass from parent" approach is also linear

[Mario Carneiro]

it's not a tree, it's a dag, and lean basically searches all paths in it

[Mario Carneiro]

so shortcut instances are incredibly bad for the algorithm

[Eric Wieser]

Is this comparison accurate to find has_coe_to_fun add_monoid_hom

Before:

• Loop over has_coe_to_fun until we find a match:
  • zero_hom.has_coe_to_fun
  • add_hom.has_coe_to_fun
  • mul_hom.has_coe_to_fun
  • add_monoid_hom.has_coe_to_fun

With the post I link to above:

• Loop over has_coe_to_fun until we find a match:
  • is_hom.has_coe_to_fun, loop over is_hom until we find a match
    • is_mul_hom.is_hom, loop over is_mul_hom until we find a match
      • is_monoid_hom.is_mul_hom
        * monoid_hom.is_monoid_hom
    • is_zero_hom.is_hom, loop over is_zero_hom until we find a match
      • is_add_monoid_hom.is_zero_hom
        * add_monoid_hom.is_add_monoid_hom
    • is_add_hom.is_hom, loop over is_add_hom until we find a match
      • is_add_monoid_hom.is_add_hom
        * add_monoid_hom.is_add_monoid_hom(I assume inference then checks for consistency?)

[Eric Wieser]

Ignoring diamonds, it looks to me like the overhead is linear in the depth of the tree, which doesn't seem too bad

[Mario Carneiro]

is is_hom just replacing all has_coe_to_fun instances then?

[Eric Wieser]

Yes, for the bundled morphisms. Things like finsupp and dfinsupp will keep using has_coe_to_fun directly of course

[Mario Carneiro]

you have is_add_monoid_hom.is_zero_hom, does that mean there is also is_add_monoid_hom?

[Mario Carneiro]

so add_monoid_hom.is_add_monoid_hom is getting tested twice

[Eric Wieser]

Yes, because there is a diamond

[Mario Carneiro]

and everything under that diamond will be doubled

[Eric Wieser]

Indeed

[Mario Carneiro]

it sounds like there is still a lurking exponential in this plan then

[Eric Wieser]

Does lean keep looking for a match in other branches even after it finds one?

[Mario Carneiro]

no, but a success can come anywhere in the tree, and unsuccessful searches have to run the gamut

[Mario Carneiro]

unsuccessful searches include unsuspecting files that have nothing to do with homs

[Kevin Buzzard]

Mario Carneiro said:

I'm pretty sure [typeclass searches are] responsible for half of mathlib's compile time (the other half being VM evaluation)

interesting you should say that...

[Eric Wieser]

Is the search breadth-first or depth-first?

[Mario Carneiro]

depth first

[Mario Carneiro]

it really is objectively not a very good algorithm

[Johan Commelin]

Is it objectively hard to improve it for lean-3.24.0?

[Mario Carneiro]

Daniel Selsam has a paper on the new typeclass algorithm in lean 4

[Johan Commelin]

Can we backport it?

[Mario Carneiro]

Johan Commelin said:

Is it objectively hard to improve it for lean-3.24.0?

It's possible

[Eric Wieser]

If lean 4 fixes things, would it be better to use the design with less human overhead, and hope that the performance issue goes away eventually?

[Mario Carneiro]

it would require some work and people will probably consider it wasted in light of lean 4

[Mario Carneiro]

it's difficult to ignore exponential factors even "temporarily"

[Johan Commelin]

I have no idea how hard it is to do something like that... If it is 1 week of work, it might be worth it. We could consider it part of the port to Lean 4...

[Eric Wieser]

How easy is it to check whether the effect is actually exponential?

[Mario Carneiro]

also we still don't even have a release date for lean 4 and many things are still up in the air so I'm not a fan of arguments for an uncertain future

[Mario Carneiro]

There are simple typeclass problems you can set up that have literal exponential search length

[Eric Wieser]

For sure - my question is how we prove that the change suggested above is one of them

[Mario Carneiro]

For a fixed size of course it's not exponential, it's just slightly bigger

[Mario Carneiro]

but it scales worse and mathlib has real scaling issues in this area

[Gabriel Ebner]

The danger of exponential searches is significantly reduced since we have caching now.

[Gabriel Ebner]

Both Lean 3's and Lean 4's type class algorithms are Turing-complete, I don't think either of them provide good performance guarantees.

[Eric Wieser]

As it turns out there are lots of diamonds in the heirarchy of morphisms: image.png

[Johan Commelin]

/me is not surprised :wink:

[Eric Wieser]

Where gray arrows are the ones that aren't actual extends clauses

[Johan Commelin]

:rofl: The graph suggests that we are missing arrows from alg_hom to add_equiv and from ring_hom to equiv.

[Eric Wieser]

Perhaps clearer with the equivs separated:

image.png

[Mario Carneiro]

Yes, the reason this is a problem is because there are in fact many diamonds in most typeclass problems, it's not a theoretical concern

[Eric Wieser]

Note also that N is 8 not 5 for zero_hom

[Mario Carneiro]

12 counting diamonds

[Eric Wieser]

For type class resolution, shouldn't only the number of edges matter?

[Eric Wieser]

Ah, which is 13

[Mario Carneiro]

I'm counting nodes

[Eric Wieser]

Shouldn't caching prevent a node being visited twice?

[Mario Carneiro]

possibly; there are situations where it won't because of undetermined metavariables I think

[Mario Carneiro]

not to mention if you have a sequence of typeclasses like foo n -> foo (n + 1)

[Mario Carneiro]

I forgot about gabriel's (heroic!) work to add caching, which solves many of the problems in this area, but because of the free form nature of typeclasses it's hard to get good guarantees

[Johan Commelin]

Are the discrimination trees in Lean 4 going to solve this issue? If we have

(f : A -> B) [is_group_hom f] : f (x * y) = f x * f y

should this just work in Lean 4? Because if I understand it correctly, simp will not just look at the head symbol, but also at *, a bit further down the tree.

[Eric Wieser]

Even if it did, presumably we'll still be stuck with function composition?

[Eric Wieser]

(https://leanprover-community.github.io/mathlib_docs/notes.html#no%20instance%20on%20morphisms)

[Anne Baanen]

I had a bit of time last week to test this idea for real, but didn't get around to writing out a report. Because the topic came up in a lean4 thread, here's my observations:

[Anne Baanen]

• Overall, using the hom typeclasses works quite well with tactics, you can just write simp [map_mul f] without worrying whether f is a mul_hom, monoid_hom, monoid_with_zero_hom, ring_hom, ...
• The to_fun class caused a few weird timeouts in simp, until I disabled the simp lemma coe_fn_coe_base
• has_coe_to_fun causes the expected type to be elaborated a bit too late, so you have to insert type hints when there is reduction going on in the type. I expect this will be better in Lean 4 because it can delay subgoals (is this correct?)
• I wanted to time whether simp gets faster because it doesn't go through all foo_hom.map_bar lemmas for every coe_fn, but didn't have the time yet
• There is still a bit of boilerplate because you have to define the foo_hom structure and the foo_hom_class with the appropriate instances, but this is only linear in the number of foos and should be automatable.

[Eric Wieser]

This pattern of having structure foo and class foo_class feels like it's essentially building the virtual "method" dispatch of C++, where foo_class is sort of like the vtable.

[Anne Baanen]

I would say it's more like the class Foo + interface IFoo pattern in Java, but yes, basically that :)

[Johan Commelin]

@Anne Baanen Thanks a lot for looking into this!

[Anne Baanen]

I revived my experiment and opened #9888. It still needs some cleaning up, but the basic idea seems to work well.

[Kyle Miller]

This is very interesting to see -- I hadn't realized morphisms have the same sort of design considerations as graphs! In an old branch for simple graphs I came up with the same design. I didn't think I could justify the complexity quite yet (nor did I think about it as the class+interface pattern), so we went with the more straightforward definition first, though I do plan to revisit this once we have more types of combinatorial objects.

These are the definitions in that branch:

class simple_graphs (α : Type u) :=
(V : α → Type v)
(adj : Π (G : α), V G → V G → Prop)
(symm : Π (G : α), symmetric (adj G))
(loopless : Π (G : α), irreflexive (adj G))

structure from_rel (V : Type u) :=
(rel : V → V → Prop)
(sym : symmetric rel)
(irr : irreflexive rel)

instance (V : Type u) : simple_graphs (from_rel V) :=
{ V := λ _, V,
  adj := from_rel.rel,
  symm := from_rel.sym,
  loopless := from_rel.irr }

To talk about a particular generic graph you could do {α : Type u} [simple_graphs α] (G : α). (I think I like the simple_graph_class and simple_graph naming convention better.) One downside is it seems this design pattern loses out on a lot of dot notation...

[Yury G. Kudryashov]

Do you think that we need [*_hom_class]? Why not just [map_zero_class] [map_add_class] etc?

[Yury G. Kudryashov]

An attribute can create a fun_like instance and [map*_class] instances.

[Anne Baanen]

The drawback of only having map_{one,mul,zero,add}_classes is that terms can grow exponentially big. This is also one of the reasons monoid bundles everything into one class instead of something like [has_one] [has_mul] [mul_assoc] [mul_one].

[Anne Baanen]

https://www.ralfj.de/blog/2019/05/15/typeclasses-exponential-blowup.html

[Yury G. Kudryashov]

In this example group takes monoid as a parameter.

[Yury G. Kudryashov]

Does the same happen with [map_*_class]? Why?

[Yury G. Kudryashov]

OTOH, with *_hom_class, in order to apply map_add, Lean has to go up in the TC hierarchy to an appropriate class, then insert *_hom_class.to_*_hom_class.....map_add in the proof term instead of something like linear_map.map_add_class.

[Eric Wieser]

I agree, I think we might be able to get away with separate classes for each map method after all

[Anne Baanen]

#9888 builds (see commit 4c51e75fe10fd6e74fb3ceb4aa0f5c5ecbbe3412), so I went ahead and cleaned up the commits; hopefully that didn't break anything.

[Anne Baanen]

Yury G. Kudryashov said:

Does the same happen with [map_*_class]? Why?

Good question! Perhaps not, since there won't be a class depending on the fields of all previous classes, in the way comm_group depends on everything in group. I'll see if I can make a good comparison.

[Anne Baanen]

Still, by completely separating into map_*_classes, we turn this:

lemma hom_eval₂ {G : Type*} [ring_hom_class G S T]
  (g : G) (x : S) : g (p.eval₂ f x) = p.eval₂ (g.comp f) (g x) := _

into this:

lemma hom_eval₂ {G : Type*} [map_add_class G S T] [map_zero_class G S T] [map_mul_class G S T] [map_one_class G S T]
  (g : G) (x : S) : g (p.eval₂ f x) = p.eval₂ (g.comp f) (g x) := _

which I wouldn't like to do...

[Anne Baanen]

Updated #9888 to resolve a merge conflict.

[Anne Baanen]

I also tried to use unbundled classes see commit 7799c4922f, but I'm getting some errors I don't understand:

def monoid_with_zero_hom.comp [mul_zero_one_class M] [mul_zero_one_class N] [mul_zero_one_class P]
  (hnp : monoid_with_zero_hom N P) (hmn : monoid_with_zero_hom M N) : monoid_with_zero_hom M P :=
{ to_fun := hnp ∘ hmn, map_zero' := by simp, map_one' := by simp,
  map_mul' := λ x y, by rw [function.comp_app, map_mul] }
/-
▶ 621:25-621:26: error:
invalid rewrite tactic, failed to synthesize type class instance for
  mul_hom_class (monoid_with_zero_hom M N) M N
state:
M : Type u_1,
N : Type u_2,
P : Type u_3,
_inst_1 : mul_zero_one_class M,
_inst_2 : mul_zero_one_class N,
_inst_3 : mul_zero_one_class P,
hnp : monoid_with_zero_hom N P,
hmn : monoid_with_zero_hom M N,
x y : M
⊢ ⇑hnp (⇑hmn (x * y)) = (⇑hnp ∘ ⇑hmn) x * (⇑hnp ∘ ⇑hmn) y
-/

[Eric Wieser]

What does set_option pp.implicit true show as the message? And what does #check @the_instance_you_expect_it_to_find give?

[Anne Baanen]

#print monoid_with_zero_hom.mul_hom_class is an instance, as expected, and it can be found when explicitly calling apply_instance:

/-- Composition of `monoid_with_zero_hom`s as a `monoid_with_zero_hom`. -/
def monoid_with_zero_hom.comp [mul_zero_one_class M] [mul_zero_one_class N] [mul_zero_one_class P]
  (hnp : monoid_with_zero_hom N P) (hmn : monoid_with_zero_hom M N) : monoid_with_zero_hom M P :=
{ to_fun := hnp ∘ hmn, map_zero' := by simp, map_one' := by simp,
  map_mul' := λ x y, begin
    rw [function.comp_app, @@map_mul _ _ _ (id _)],
    swap 3, { apply_instance },
    simp
  end}

[Anne Baanen]

pp.implicit gives a totally normal instance:

invalid rewrite tactic, failed to synthesize type class instance for
  @mul_hom_class (@monoid_with_zero_hom M N _inst_1 _inst_2) M N
    (@mul_one_class.to_has_mul M (@mul_zero_one_class.to_mul_one_class M _inst_1))
    (@mul_zero_class.to_has_mul N (@mul_zero_one_class.to_mul_zero_class N _inst_2))
    (@monoid_with_zero_hom.fun_like M N _inst_1 _inst_2)

[Anne Baanen]

Also:

    have : @mul_hom_class (@monoid_with_zero_hom M N _inst_1 _inst_2) M N
      (@mul_one_class.to_has_mul M (@mul_zero_one_class.to_mul_one_class M _inst_1))
      (@mul_zero_class.to_has_mul N (@mul_zero_one_class.to_mul_zero_class N _inst_2))
      (@monoid_with_zero_hom.fun_like M N _inst_1 _inst_2) := by apply_instance, -- works
    rw [function.comp_app, map_mul], -- fails

[Anne Baanen]

Although replacing have with haveI will make it work amazingly enough!

[Anne Baanen]

In any case, as long as we don't have any way to abbreviate [fun_like F A B] [mul_hom_class F A B] [one_hom_class F A B] [add_hom_class F A B] [zero_hom_class F A B] into something as concise as [ring_hom_class F A B], I don't think unbundling is the way to go.

[Anne Baanen]

(I'd be okay with unbundling the extends has_coe_to_fun or extends fun_like parts into a parameter - that would separate data from proofs.)

[Anne Baanen]

In a related note, I have been running into issues where ideal.quotient, submodule.quotient and subgroup.quotient don't behave identically although they have equivalent definitions. What if we made a subgroup_class extending set_like and defined quotient in terms of that...

[Eric Wieser]

Here's where we're at now:

image.png

[Eric Rodriguez]

can you upload a higher quality verison of that?

[Eric Wieser]

It's in the center of https://gist.githubusercontent.com/eric-wieser/479c49a306430d9d8a896f105ef32178/raw/32f67356bac21dda2c9a80a99d6cef602b643d96/out-small.svg

[Eric Rodriguez]

weird that some of them don't extend fun_like...

[Eric Rodriguez]

docs#order_hom_class, docs#continuous_map_class

[Eric Wieser]

That's a data parsing error because order_hom_class is an abbreviation

[Eric Rodriguez]

continuous_map_class does too, but it seems in a new-style way?

[Eric Wieser]

That one's a mystery to me

[Eric Wieser]

Feel free to try and adjust the script

[Yakov Pechersky]

What about the arrows that terminate into space here?
image.png

[Eric Wieser]

Click on them

[Yakov Pechersky]

I see, so the TC "values" are the arrow ends, the boxes are the defs of the class