Zulip Chat Archive

Stream: general

Topic: Typeclasses for morphisms


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Reid Barton (Oct 13 2020 at 18:27):

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

view this post on Zulip 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

view this post on Zulip 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".

view this post on Zulip Yury G. Kudryashov (Oct 13 2020 at 18:42):

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

view this post on Zulip 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].

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Adam Topaz (Oct 13 2020 at 22:52):

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

view this post on Zulip Adam Topaz (Oct 13 2020 at 22:52):

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

view this post on Zulip Eric Wieser (Oct 13 2020 at 22:53):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Oct 23 2020 at 16:32):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip Anne Baanen (Nov 03 2020 at 09:31):

You're right :face_palm:

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Anne Baanen (Nov 03 2020 at 09:36):

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

view this post on Zulip 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.

view this post on Zulip 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!)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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]?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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'

view this post on Zulip Eric Wieser (Nov 03 2020 at 11:27):

Can you make is_zero_hom extend has_coe_to_fun somehow?

view this post on Zulip Eric Wieser (Nov 03 2020 at 11:27):

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

view this post on Zulip 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)

view this post on Zulip Anne Baanen (Nov 03 2020 at 11:28):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 03 2020 at 11:50):

Having is_zero_hom extend is_hom didn't work?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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*)`

view this post on Zulip Anne Baanen (Nov 03 2020 at 12:01):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 03 2020 at 12:04):

Is add_monoid_hom.is_hom needed there?

view this post on Zulip Anne Baanen (Nov 03 2020 at 12:05):

We can delete it, indeed.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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} ( : c α) ( : c β), hom    α  β)
(id : Π {α : Type u} (I : c α), hom I I)
(comp : Π {α β γ : Type u} ( : c α) ( : c β) ( : c γ),
  hom    hom    hom  )
(hom_ext :  {α β : Type u} ( : c α) ( : c β), function.injective (to_fun  ) . obviously)
(id_to_fun :  {α : Type u} (I : c α), to_fun I I (id I) = _root_.id . obviously)
(comp_to_fun :  {α β γ : Type u} ( : c α) ( : c β) ( : c γ)
  (f : hom  ) (g : hom  ),
  to_fun   (comp    g f) = (to_fun   g)  (to_fun   f) . obviously)

view this post on Zulip Anne Baanen (Nov 03 2020 at 12:16):

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

view this post on Zulip 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

view this post on Zulip 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 :(

view this post on Zulip Eric Wieser (Nov 03 2020 at 12:18):

Exactly

view this post on Zulip Eric Wieser (Nov 03 2020 at 12:19):

docs#category_theory.bundled_hom since I'm lazy

view this post on Zulip Eric Wieser (Nov 03 2020 at 12:21):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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. :(

view this post on Zulip Eric Wieser (Nov 03 2020 at 12:50):

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

view this post on Zulip 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".

view this post on Zulip Yury G. Kudryashov (Nov 03 2020 at 13:14):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Anne Baanen (Nov 03 2020 at 13:55):

Or would there be another issue I'm missing?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 03 2020 at 14:29):

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

view this post on Zulip Mario Carneiro (Nov 03 2020 at 14:30):

I see anne suggesting a lot more than that

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 03 2020 at 14:31):

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

view this post on Zulip Mario Carneiro (Nov 03 2020 at 14:31):

this will make the typeclass problem a lot harder

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 03 2020 at 14:32):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 03 2020 at 14:33):

it will slow it down

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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, ...)"

view this post on Zulip Mario Carneiro (Nov 03 2020 at 14:37):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 03 2020 at 14:45):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 03 2020 at 14:49):

only if it comes up for something else

view this post on Zulip Mario Carneiro (Nov 03 2020 at 14:50):

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

view this post on Zulip Mario Carneiro (Nov 03 2020 at 14:50):

this keeps the typeclass problem very local

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 03 2020 at 14:51):

yes

view this post on Zulip Eric Wieser (Nov 03 2020 at 14:51):

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

view this post on Zulip Mario Carneiro (Nov 03 2020 at 14:51):

yes, it's quadratic in 5

view this post on Zulip Eric Wieser (Nov 03 2020 at 14:51):

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

view this post on Zulip Mario Carneiro (Nov 03 2020 at 14:52):

however, individual typeclass problems are only linear in 5

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 03 2020 at 14:53):

Why is the current situation exponential anyway?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 03 2020 at 14:55):

so shortcut instances are incredibly bad for the algorithm

view this post on Zulip 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?)

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 03 2020 at 14:57):

is is_hom just replacing all has_coe_to_fun instances then?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 03 2020 at 15:00):

so add_monoid_hom.is_add_monoid_hom is getting tested twice

view this post on Zulip Eric Wieser (Nov 03 2020 at 15:00):

Yes, because there is a diamond

view this post on Zulip Mario Carneiro (Nov 03 2020 at 15:01):

and everything under that diamond will be doubled

view this post on Zulip Eric Wieser (Nov 03 2020 at 15:01):

Indeed

view this post on Zulip Mario Carneiro (Nov 03 2020 at 15:01):

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

view this post on Zulip Eric Wieser (Nov 03 2020 at 15:01):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 03 2020 at 15:02):

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

view this post on Zulip 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...

view this post on Zulip Eric Wieser (Nov 03 2020 at 15:03):

Is the search breadth-first or depth-first?

view this post on Zulip Mario Carneiro (Nov 03 2020 at 15:03):

depth first

view this post on Zulip Mario Carneiro (Nov 03 2020 at 15:04):

it really is objectively not a very good algorithm

view this post on Zulip Johan Commelin (Nov 03 2020 at 15:04):

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

view this post on Zulip Mario Carneiro (Nov 03 2020 at 15:04):

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

view this post on Zulip Johan Commelin (Nov 03 2020 at 15:05):

Can we backport it?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 03 2020 at 15:06):

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

view this post on Zulip 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...

view this post on Zulip Eric Wieser (Nov 03 2020 at 15:07):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 03 2020 at 15:08):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 03 2020 at 15:09):

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

view this post on Zulip Mario Carneiro (Nov 03 2020 at 15:09):

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

view this post on Zulip Gabriel Ebner (Nov 03 2020 at 15:10):

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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Nov 03 2020 at 15:26):

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

view this post on Zulip Johan Commelin (Nov 03 2020 at 15:26):

/me is not surprised :wink:

view this post on Zulip Eric Wieser (Nov 03 2020 at 15:26):

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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Nov 03 2020 at 15:30):

Perhaps clearer with the equivs separated:

image.png

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 03 2020 at 15:33):

Note also that N is 8 not 5 for zero_hom

view this post on Zulip Mario Carneiro (Nov 03 2020 at 15:36):

12 counting diamonds

view this post on Zulip Eric Wieser (Nov 03 2020 at 15:37):

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

view this post on Zulip Eric Wieser (Nov 03 2020 at 15:38):

Ah, which is 13

view this post on Zulip Mario Carneiro (Nov 03 2020 at 15:38):

I'm counting nodes

view this post on Zulip Eric Wieser (Nov 03 2020 at 15:38):

Shouldn't caching prevent a node being visited twice?

view this post on Zulip Mario Carneiro (Nov 03 2020 at 15:39):

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

view this post on Zulip Mario Carneiro (Nov 03 2020 at 15:39):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Mar 04 2021 at 10:08):

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

view this post on Zulip Eric Wieser (Mar 04 2021 at 10:09):

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

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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