Zulip Chat Archive

Stream: general

Topic: id in classes


view this post on Zulip Sebastien Gouezel (Jun 11 2020 at 17:05):

I don't really remember if having useless id in typeclasses can be bad for typeclass inference or not. For instance in

#print power_series.ring

@[instance]
protected noncomputable def power_series.ring : Π {α : Type u_1} [_inst_1 : ring α], ring (power_series α) :=
λ {α : Type u_1} [_inst_1 : ring α], id mv_power_series.ring

Thoughts?

view this post on Zulip Reid Barton (Jun 11 2020 at 17:05):

It does have a (probably bad) effect, yes.

view this post on Zulip Reid Barton (Jun 11 2020 at 17:15):

Namely, if this instance power_series.ring itself appears in the type of an instance search problem (maybe for a class like class fancy_ring (A : Type) [ring A] := ..., although this is not so common in the algebraic hierarchy, I suppose), then instance search will not be able to see that power_series.ring is actually equal to mv_power_series.ring so it won't apply instances that are declared for the latter.

view this post on Zulip Patrick Massot (Jun 11 2020 at 17:38):

Isn't hiding stuff the goal of such an instance?

view this post on Zulip Mario Carneiro (Jun 11 2020 at 17:42):

I don't think id has instance reducibility

view this post on Zulip Mario Carneiro (Jun 11 2020 at 17:43):

it is as opaque as a regular definition

view this post on Zulip Mario Carneiro (Jun 11 2020 at 17:44):

I think this comes up when you are trying to prove that some defeq diamond commutes

view this post on Zulip Reid Barton (Jun 11 2020 at 17:44):

It's not easy to come up with an example where it would matter here because I guess power_series must be defined by something like def power_series := mv_power_series unit, and this def also doesn't have instance reducibility.

view this post on Zulip Mario Carneiro (Jun 11 2020 at 17:45):

it shouldn't hamper regular instance search

view this post on Zulip Mario Carneiro (Jun 11 2020 at 17:47):

A recent norm_num bug had to do with a problem of this form, where int.has_sub is defeq to algebra_has_sub but the defeq is only if you unfold semireducible definitions so lean prefers to unfold something else

view this post on Zulip Gabriel Ebner (Jun 11 2020 at 17:48):

The typical way this burns you is if you have a second ring instance for power_series, like:

instance : comm_ring (power_series α) := mv_power_series.comm_ring

view this post on Zulip Sebastien Gouezel (Jun 11 2020 at 18:17):

You have, among many instances,

instance [semiring α]        : semiring        (power_series α) := by delta power_series; apply_instance
instance [comm_semiring α]   : comm_semiring   (power_series α) := by delta power_series; apply_instance
instance [ring α]            : ring            (power_series α) := by delta power_series; apply_instance
instance [comm_ring α]       : comm_ring       (power_series α) := by delta power_series; apply_instance

view this post on Zulip Johan Commelin (Jun 11 2020 at 18:19):

O.ooo... did I create a mess?

view this post on Zulip Sebastien Gouezel (Jun 11 2020 at 18:31):

#3033 (not sure it is really useful, but I don't think it can hurt).

view this post on Zulip Gabriel Ebner (Jun 11 2020 at 19:23):

It's typically not a problem because type-class instances usually occur in implicit arguments (and implicit arguments are unified with a higher transparency setting, i.e., semireducible). The last time I've seen this issue is with the bundled structure from the category theory library (where the type-class instance is explicit). Maybe the conclusion here is to make bundled.str instance-implicit.

view this post on Zulip Mario Carneiro (Jun 11 2020 at 19:30):

The clean tactic is intended for just this purpose

view this post on Zulip Mario Carneiro (Jun 11 2020 at 19:31):

it removes identity functions inserted to the term by tactics that do definitional reduction


Last updated: May 06 2021 at 21:09 UTC