# Zulip Chat Archive

## 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 :=
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 (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_hom`

s, 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_param`

s 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 -/
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 (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 -/
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 (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 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 (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 u`

s have a zero :(

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

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

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

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

#### 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`

?

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

yes

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

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

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

yes, it's quadratic in 5

#### 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

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

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?

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

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:

#### 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?

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

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?

#### Eric Wieser (Mar 04 2021 at 10:09):

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

#### 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`foo`

s 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