## Stream: general

### Topic: Typeclasses for morphisms

#### Eric Wieser (Oct 13 2020 at 16:45):

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 :=
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 (Oct 13 2020 at 18:18):

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 (Oct 13 2020 at 18:19):

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 (Oct 13 2020 at 18:27):

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 (Oct 13 2020 at 18:27):

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

#### Reid Barton (Oct 13 2020 at 18:32):

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 (Oct 13 2020 at 18:42):

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 (Oct 13 2020 at 18:42):

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

#### Yury G. Kudryashov (Oct 13 2020 at 18:43):

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

#### Eric Wieser (Oct 13 2020 at 22:45):

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

#### Kevin Buzzard (Oct 13 2020 at 22:49):

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 (Oct 13 2020 at 22:51):

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

#### Adam Topaz (Oct 13 2020 at 22:52):

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

#### Adam Topaz (Oct 13 2020 at 22:52):

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

#### Eric Wieser (Oct 13 2020 at 22:53):

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

#### Chris Hughes (Oct 13 2020 at 23:11):

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 (Oct 23 2020 at 13:33):

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 (Oct 23 2020 at 15:36):

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 (Oct 23 2020 at 15:37):

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

#### Eric Wieser (Oct 23 2020 at 15:43):

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

#### Yury G. Kudryashov (Oct 23 2020 at 15:50):

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

#### Eric Wieser (Oct 23 2020 at 15:52):

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 (Oct 23 2020 at 16:32):

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

#### Anne Baanen (Nov 03 2020 at 09:24):

@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 (Nov 03 2020 at 09:28):

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 (Nov 03 2020 at 09:29):

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 (Nov 03 2020 at 09:30):

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

#### Anne Baanen (Nov 03 2020 at 09:31):

You're right :face_palm:

#### Eric Wieser (Nov 03 2020 at 09:33):

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

#### Anne Baanen (Nov 03 2020 at 09:35):

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 (Nov 03 2020 at 09:36):

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

#### Sebastien Gouezel (Nov 03 2020 at 09:42):

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 (Nov 03 2020 at 09:45):

(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 (Nov 03 2020 at 09:46):

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

#### Anne Baanen (Nov 03 2020 at 09:47):

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 (Nov 03 2020 at 09:48):

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

#### Anne Baanen (Nov 03 2020 at 09:52):

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 (Nov 03 2020 at 09:53):

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 (Nov 03 2020 at 09:54):

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 (Nov 03 2020 at 09:57):

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

#### Anne Baanen (Nov 03 2020 at 09:59):

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 (Nov 03 2020 at 11:21):

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 (Nov 03 2020 at 11:27):

Can you make is_zero_hom extend has_coe_to_fun somehow?

#### Eric Wieser (Nov 03 2020 at 11:27):

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

#### Anne Baanen (Nov 03 2020 at 11:28):

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 (Nov 03 2020 at 11:28):

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

#### Anne Baanen (Nov 03 2020 at 11:36):

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 -/
(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. -/
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 (Nov 03 2020 at 11:50): Having is_zero_hom extend is_hom didn't work? #### Anne Baanen (Nov 03 2020 at 11:51): 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 (Nov 03 2020 at 11:55): 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 (Nov 03 2020 at 11:56): 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 (Nov 03 2020 at 12:01):

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 (Nov 03 2020 at 12:01):

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

#### Anne Baanen (Nov 03 2020 at 12:04):

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 -/
(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. -/
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

is_add_monoid_hom (M →+ N) M N :=
{ coe := λ f, f.to_fun,
map_zero := λ f, f.map_zero',

section test

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 (Nov 03 2020 at 12:04):

Is add_monoid_hom.is_hom  needed there?

#### Anne Baanen (Nov 03 2020 at 12:05):

We can delete it, indeed.

#### Eric Wieser (Nov 03 2020 at 12:08):

And I suppose

example [add_monoid M] [add_monoid N] {hom1 : Type*} {hom2 : Type*}
[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 (Nov 03 2020 at 12:13):

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 (Nov 03 2020 at 12:14):

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

#### Anne Baanen (Nov 03 2020 at 12:15):

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 (Nov 03 2020 at 12:16):

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

#### Eric Wieser (Nov 03 2020 at 12:17):

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 (Nov 03 2020 at 12:18):

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

Exactly

#### Eric Wieser (Nov 03 2020 at 12:19):

docs#category_theory.bundled_hom since I'm lazy

#### Eric Wieser (Nov 03 2020 at 12:21):

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

#### Eric Wieser (Nov 03 2020 at 12:24):

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 (Nov 03 2020 at 12:26):

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 (Nov 03 2020 at 12:28):

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 (Nov 03 2020 at 12:30):

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. :(

#### Yury G. Kudryashov (Nov 03 2020 at 13:13):

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 (Nov 03 2020 at 13:14):

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

#### Eric Wieser (Nov 03 2020 at 13:20):

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

#### Anne Baanen (Nov 03 2020 at 13:54):

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 (Nov 03 2020 at 13:55):

Or would there be another issue I'm missing?

#### Kevin Buzzard (Nov 03 2020 at 14:11):

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 (Nov 03 2020 at 14:12):

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 (Nov 03 2020 at 14:24):

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

#### Anne Baanen (Nov 03 2020 at 14:25):

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 (Nov 03 2020 at 14:28):

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 (Nov 03 2020 at 14:29):

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

#### Mario Carneiro (Nov 03 2020 at 14:30):

I see anne suggesting a lot more than that

#### Eric Wieser (Nov 03 2020 at 14:30):

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 (Nov 03 2020 at 14:31):

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

#### Mario Carneiro (Nov 03 2020 at 14:31):

this will make the typeclass problem a lot harder

#### Eric Wieser (Nov 03 2020 at 14:32):

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 (Nov 03 2020 at 14:32):

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

#### Eric Wieser (Nov 03 2020 at 14:33):

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 (Nov 03 2020 at 14:33):

it will slow it down

#### Eric Wieser (Nov 03 2020 at 14:34):

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

#### Mario Carneiro (Nov 03 2020 at 14:35):

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

#### Eric Wieser (Nov 03 2020 at 14:36):

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

#### Eric Wieser (Nov 03 2020 at 14:36):

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 (Nov 03 2020 at 14:37):

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

#### Mario Carneiro (Nov 03 2020 at 14:38):

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

#### Mario Carneiro (Nov 03 2020 at 14:39):

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 (Nov 03 2020 at 14:41):

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

#### Mario Carneiro (Nov 03 2020 at 14:42):

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

#### Mario Carneiro (Nov 03 2020 at 14:43):

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

#### Mario Carneiro (Nov 03 2020 at 14:44):

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 (Nov 03 2020 at 14:45):

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

#### Eric Wieser (Nov 03 2020 at 14:48):

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 (Nov 03 2020 at 14:49):

only if it comes up for something else

#### Mario Carneiro (Nov 03 2020 at 14:50):

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

#### Mario Carneiro (Nov 03 2020 at 14:50):

this keeps the typeclass problem very local

#### Eric Wieser (Nov 03 2020 at 14:51):

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

yes

#### Eric Wieser (Nov 03 2020 at 14:51):

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

#### Eric Wieser (Nov 03 2020 at 14:51):

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

#### Mario Carneiro (Nov 03 2020 at 14:52):

however, individual typeclass problems are only linear in 5

#### Mario Carneiro (Nov 03 2020 at 14:53):

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 (Nov 03 2020 at 14:53):

Why is the current situation exponential anyway?

#### Mario Carneiro (Nov 03 2020 at 14:54):

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

#### Eric Wieser (Nov 03 2020 at 14:54):

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

#### Mario Carneiro (Nov 03 2020 at 14:54):

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

#### Mario Carneiro (Nov 03 2020 at 14:55):

so shortcut instances are incredibly bad for the algorithm

#### Eric Wieser (Nov 03 2020 at 14:55):

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 (Nov 03 2020 at 14:56):

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 (Nov 03 2020 at 14:57):

is is_hom just replacing all has_coe_to_fun instances then?

#### Eric Wieser (Nov 03 2020 at 14:58):

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

#### Mario Carneiro (Nov 03 2020 at 14:59):

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

#### Mario Carneiro (Nov 03 2020 at 15:00):

so add_monoid_hom.is_add_monoid_hom is getting tested twice

#### Eric Wieser (Nov 03 2020 at 15:00):

Yes, because there is a diamond

#### Mario Carneiro (Nov 03 2020 at 15:01):

and everything under that diamond will be doubled

Indeed

#### Mario Carneiro (Nov 03 2020 at 15:01):

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

#### Eric Wieser (Nov 03 2020 at 15:01):

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

#### Mario Carneiro (Nov 03 2020 at 15:02):

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

#### Mario Carneiro (Nov 03 2020 at 15:02):

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

#### Kevin Buzzard (Nov 03 2020 at 15:02):

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 (Nov 03 2020 at 15:03):

Is the search breadth-first or depth-first?

depth first

#### Mario Carneiro (Nov 03 2020 at 15:04):

it really is objectively not a very good algorithm

#### Johan Commelin (Nov 03 2020 at 15:04):

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

#### Mario Carneiro (Nov 03 2020 at 15:04):

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

#### Johan Commelin (Nov 03 2020 at 15:05):

Can we backport it?

#### Mario Carneiro (Nov 03 2020 at 15:05):

Johan Commelin said:

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

It's possible

#### Eric Wieser (Nov 03 2020 at 15:05):

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 (Nov 03 2020 at 15:05):

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

#### Mario Carneiro (Nov 03 2020 at 15:06):

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

#### Johan Commelin (Nov 03 2020 at 15:06):

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 (Nov 03 2020 at 15:07):

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

#### Mario Carneiro (Nov 03 2020 at 15:07):

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 (Nov 03 2020 at 15:08):

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

#### Eric Wieser (Nov 03 2020 at 15:08):

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

#### Mario Carneiro (Nov 03 2020 at 15:09):

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

#### Mario Carneiro (Nov 03 2020 at 15:09):

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

#### Gabriel Ebner (Nov 03 2020 at 15:10):

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

#### Gabriel Ebner (Nov 03 2020 at 15:11):

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 (Nov 03 2020 at 15:26):

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

#### Johan Commelin (Nov 03 2020 at 15:26):

/me is not surprised :wink:

#### Eric Wieser (Nov 03 2020 at 15:26):

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

#### Johan Commelin (Nov 03 2020 at 15:28):

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

#### Eric Wieser (Nov 03 2020 at 15:30):

Perhaps clearer with the equivs separated:

image.png

#### Mario Carneiro (Nov 03 2020 at 15:31):

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 (Nov 03 2020 at 15:33):

Note also that N is 8 not 5 for zero_hom

#### Mario Carneiro (Nov 03 2020 at 15:36):

12 counting diamonds

#### Eric Wieser (Nov 03 2020 at 15:37):

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

Ah, which is 13

#### Mario Carneiro (Nov 03 2020 at 15:38):

I'm counting nodes

#### Eric Wieser (Nov 03 2020 at 15:38):

Shouldn't caching prevent a node being visited twice?

#### Mario Carneiro (Nov 03 2020 at 15:39):

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

#### Mario Carneiro (Nov 03 2020 at 15:39):

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

#### Mario Carneiro (Nov 03 2020 at 15:41):

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 (Mar 04 2021 at 10:06):

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 (Mar 04 2021 at 10:08):

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

#### Anne Baanen (Mar 15 2021 at 11:54):

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 (Mar 15 2021 at 12:04):

• 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 (Mar 15 2021 at 12:08):

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 (Mar 15 2021 at 12:09):

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

#### Johan Commelin (Mar 15 2021 at 12:23):

@Anne Baanen Thanks a lot for looking into this!

Last updated: May 12 2021 at 05:19 UTC