## Stream: general

### Topic: deriving instances

#### Johan Commelin (Aug 27 2019 at 07:32):

Now and again, we define a wrapper type. (Just because we can, right?) And afterwards we have a bunch of lines reading

def my_wrapper := something
instance : comm_ring my_wrapper := by delta my_wrapper; apply_instance
instance : topological_space my_wrapper := by delta my_wrapper; apply_instance
-- ... etc ...


It would be cute if we could just write

@[derive comm_ring topological_space]
def my_wrapper := something


#### Johan Commelin (Aug 27 2019 at 07:32):

For an example, see https://github.com/leanprover-community/lean-perfectoid-spaces/blob/big-clean-up/src/Huber_ring/localization.lean#L71-L77 where @Patrick Massot wrote

/-- Topological localization A(T/s) -/
def rational_open_data.top_loc (r : rational_open_data A) := away r.s

local notation A⟮T/s⟯ := r.top_loc

meta def find_inst : tactic unit := [delta rational_open_data.top_loc away; apply_instance]

instance : comm_ring A⟮T/s⟯ := by find_inst

instance : module A A⟮T/s⟯ := by find_inst

instance : algebra A A⟮T/s⟯ := by find_inst


#### Sebastian Ullrich (Aug 27 2019 at 07:51):

You should be able to define a single derive_handler that does this

#### Scott Morrison (Aug 27 2019 at 08:19):

This does seem like a good idea! We really need to keep track of things like this. :-)

#### Rob Lewis (Aug 27 2019 at 08:21):

I don't have time right now to clean this up, but if someone feels like doing it, here's a working start:

open tactic

@[derive_handler] meta def delta_instance : derive_handler :=
λ cls tp,
(do tp' ← mk_const tp,
tgt ← to_expr (%%cls %%tp'),
(_, v) ← solve_aux tgt (delta_target [tp] >> apply_instance >> done),
v ← instantiate_mvars v,
nm ← mk_fresh_name,
add_decl \$ declaration.defn nm [] tgt v reducibility_hints.abbrev tt,
set_basic_attribute instance nm tt,
return tt) <|> return ff

@[derive [monoid, semiring]] def T := ℕ

example (a b : T) : a + b = b + a := by simp


#### Johan Commelin (Aug 27 2019 at 08:23):

Awesome! Thanks for starting this.

#### Scott Morrison (Aug 27 2019 at 08:23):

Looks lovely. Is there actually anything to do except go through the library and see where it could be used, and seeing if there are any unexpected failures?

#### Rob Lewis (Aug 27 2019 at 08:23):

If nothing else, it should generate better names for the instances.

#### Rob Lewis (Aug 27 2019 at 08:24):

I'm not sure why the instantiate_mvars is necessary but it fails without it.

#### Johan Commelin (Aug 28 2019 at 08:37):

Is someone working on this? I still don't have time to properly learn meta programming. I have no idea how to generate better names. But I wouldn't like Rob's sketch to drown in Zulip history

#### Johan Commelin (Sep 23 2019 at 13:28):

This didn't end up in mathlib yet, did it? Because I'm currently writing:

instance [add_monoid α]      : add_monoid      (power_series α) := by delta power_series; apply_instance
instance [add_group α]       : add_group       (power_series α) := by delta power_series; apply_instance
instance [add_comm_monoid α] : add_comm_monoid (power_series α) := by delta power_series; apply_instance
instance [add_comm_group α]  : add_comm_group  (power_series α) := by delta power_series; apply_instance
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
instance [nonzero_comm_ring α] : nonzero_comm_ring (power_series α) := by delta power_series; apply_instance
instance [semiring α]        : semimodule α    (power_series α) := by delta power_series; apply_instance
instance [ring α]            : module α        (power_series α) := by delta power_series; apply_instance
instance [comm_ring α]       : algebra α       (power_series α) := by delta power_series; apply_instance


#### Sebastien Gouezel (Sep 23 2019 at 13:29):

local attribute [reducible] power_series?

#### Sebastien Gouezel (Sep 23 2019 at 13:29):

I mean, to divide the length of all your proofs by 2.

#### Johan Commelin (Sep 23 2019 at 13:36):

Yeah... the issue is the number of lines (-;

#### Johan Commelin (Sep 23 2019 at 13:36):

I don't touch the proofs when I copy-paste (-;

#### Reid Barton (Sep 23 2019 at 13:50):

Did I miss this local attribute [reducible] trick becoming popular? I saw it also in #1438

#### Rob Lewis (Sep 23 2019 at 13:52):

I'll fix the naming thing and PR this, but I'm still not sure it isn't missing something.

#### Rob Lewis (Sep 23 2019 at 13:54):

Note that the derive attribute won't help with the instances with hypotheses like in your example.

#1475

#### Johan Commelin (Sep 23 2019 at 14:22):

Too bad it doesn't help with the kind of "problem" I had.

#### Scott Morrison (Sep 23 2019 at 23:04):

#1475 is awesome, but I wonder if we were a bit fast merging it. I think we should at least create an issue reminding us to actually deploy it across the library!

#### Scott Morrison (Sep 23 2019 at 23:07):

@Reid Barton, re: local attribute [reducible], I've just been getting more and more wary of relying of rfl to prove things. It feels like in so many examples we've seen it burn you later, either because Lean wanders off into "heavy refl" elaborations, or you find yourself writing things that don't quite make sense but "Lean can see what you mean" in very unintuitive ways, that are then impossible to read again later. Keeping [reducible] contained to small scopes shortly after the definition seems like a good hygiene regime --- it encourages you to get the API right at the point of definition, by preventing you from "cheating" later.

#### Reid Barton (Sep 23 2019 at 23:50):

local attribute [reducible] doesn't do that though. You can still prove that things are equal by rfl outside that scope, unless you make the definition[irreducible].

oh ... :-)

#### Scott Morrison (Sep 23 2019 at 23:57):

Maybe there is very little payoff at all, sorry.

#### Floris van Doorn (Sep 24 2019 at 01:33):

#1475 is awesome, but I wonder if we were a bit fast merging it. I think we should at least create an issue reminding us to actually deploy it across the library!

I don't think that we have to deploy a tactic in the same PR that introduces the tactic (for one: if you make the PR, often you have to make changes to the tactic, and then you might have to change the way you deploy it everywhere).

It's probably good to create an issue indeed.

#### Reid Barton (Sep 25 2019 at 16:28):

@Rob Lewis Arguably, the most correct (and simplest) way to implement this is actually to generate, for @[derive ring] def T := ℤ, the instance

instance [h : ring ℤ] : ring T := h


#### Reid Barton (Sep 25 2019 at 16:30):

That will also handle Johan's case where the instance we want to derive from has additional instance parameters, and lets us defer the decision of how to supply the original instance to the use site of the derived instance

#### Reid Barton (Sep 25 2019 at 16:30):

The downside is it means an extra step to resolve the instance

#### Rob Lewis (Sep 25 2019 at 17:38):

That derive handler would never fail, right? You can make an instance like that for any declaration. It wouldn't be hard to accidentally create one that's slow to search for and never succeeds.

#### Reid Barton (Sep 26 2019 at 23:40):

So I hadn't actually tried out this delta instance thing yet and I didn't realize it was hooked into a general @[derive] mechanism. I agree that having a derive handler that can never fail isn't ideal.
Sort of relatedly, it's a bit annoying that this thing (which I'm not sure what to call exactly) doesn't give any useful information when it fails.

#### Reid Barton (Sep 26 2019 at 23:41):

Should this work?

import data.set
@[derive has_coe_to_sort] def X : Type := set ℕ -- failed to find a derive handler for 'has_coe_to_sort'
-- instance : has_coe_to_sort X := by { delta X, apply_instance } -- works


#### Reid Barton (Sep 26 2019 at 23:43):

It works for has_inter, say, so it must be something unusual about has_coe_to_sort

#### Reid Barton (Sep 26 2019 at 23:46):

In GHC it was eventually (relatively recently) realized that sometimes you might want to specify whether to use GND (roughly equivalent to this delta_instance) or the built-in, class-specific deriving mechanism, so they added some kind of syntax to disambiguate the two mechanisms where required. But the list of classes with class-specific deriving mechanisms is fixed in GHC, so the rule "use class-specific mechanism for any class that has one, otherwise GND" worked well enough for a long time. But Lean makes the deriving mechanism extensible, so it might make more sense to use a different attribute entirely for delta_instance.

#### Reid Barton (Sep 27 2019 at 00:32):

GHC actually has a third deriving mechanism as well, which is the equivalent of instance ... : C T := {}, with the idea that all the fields will be provided by default values. I'm not sure whether that would ever be useful for us.

#### Rob Lewis (Sep 27 2019 at 09:01):

I won't have time today to look into this, but yes, that example should work. There's nothing special about using a derive handler, it could just as easily be its own attribute.

#### Rob Lewis (Sep 28 2019 at 13:52):

Should this work?

import data.set
@[derive has_coe_to_sort] def X : Type := set ℕ -- failed to find a derive handler for 'has_coe_to_sort'
-- instance : has_coe_to_sort X := by { delta X, apply_instance } -- works


This is working for me. I changed the name generation function, but not in a way that should affect this...

#### Rob Lewis (Sep 30 2019 at 08:36):

In GHC it was eventually (relatively recently) realized that sometimes you might want to specify whether to use GND (roughly equivalent to this delta_instance) or the built-in, class-specific deriving mechanism, so they added some kind of syntax to disambiguate the two mechanisms where required. But the list of classes with class-specific deriving mechanisms is fixed in GHC, so the rule "use class-specific mechanism for any class that has one, otherwise GND" worked well enough for a long time. But Lean makes the deriving mechanism extensible, so it might make more sense to use a different attribute entirely for delta_instance.

Do others have an opinion on this? I see Reid's point, but I'm not sure if/when it will come up in practice.

#### Reid Barton (Sep 30 2019 at 14:00):

To clarify and relate to what I wrote earlier, the problem isn't so much that the end user really might want to make a decision between two methods of deriving (though it is possible), but that when delta_handler fails for some reason, it can't tell whether the user was trying to use it or some class-specific deriving method which will be tried later, so it can't do proper error reporting.

#### Reid Barton (Sep 30 2019 at 14:07):

For @[derive] Lean tries all registered derive handles with no guarantees about the order, right?

#### Rob Lewis (Sep 30 2019 at 14:11):

Okay, I see what you mean. There are two failure modes for derive handlers. Returning ff means "this derive handler doesn't apply to this instance," and failing means "this handler should have worked but something went wrong." But delta_instance can never fail because we don't know if it should work or not.

#### Rob Lewis (Sep 30 2019 at 14:12):

I think it's kind of a shame. Two different attributes that both mean "find an instance of this" is pretty ugly.

#### Rob Lewis (Sep 30 2019 at 14:14):

As far as I can tell there's no way to force a certain order on the derive handlers. They come in the order the attribute manager gives them, which is probably most recently declared first?

#### Sebastian Ullrich (Sep 30 2019 at 14:16):

Priority first, most recent secondary

#### Rob Lewis (Sep 30 2019 at 14:18):

Oh, nice. Then we could set delta_instance to priority 10.

#### Sebastian Ullrich (Sep 30 2019 at 14:22):

When I wrote the derive handlers API, it did not occur to me that there would be reasonable handlers apart from delta_instance for a def. I only skimmed this thread, do you have such an example?

#### Johan Commelin (Sep 30 2019 at 14:24):

Is the recently added simps an example?

#### Johan Commelin (Sep 30 2019 at 14:25):

It derives simp-lemmas when defining terms of a type that is a structure

#### Reid Barton (Sep 30 2019 at 14:28):

Maybe decidable? This isn't quite a real answer because the solution there would be to use delta_instance plus the existing decidable instances, but it feels close.

#### Rob Lewis (Sep 30 2019 at 14:28):

Hmm, but just running delta_instance last won't work either, e.g.

@[derive decidable_eq] def S := ℕ


#### Reid Barton (Sep 30 2019 at 14:29):

Oh interesting example. So here the handler for decidable_eq runs and it "knows" it is the correct handler so it fails rather than letting delta_instance run

#### Rob Lewis (Sep 30 2019 at 14:32):

Right. I think a generic handler like delta_instance just doesn't fit into @Sebastian Ullrich 's framework. So maybe it is better as a separate attribute.

#### Reid Barton (Sep 30 2019 at 14:34):

Another possibility is we give delta_instance the highest priority and have it assume it's the right handler if and only if it's applied to a def (assuming it can check that). But it feels like a bit of a hack

#### Rob Lewis (Sep 30 2019 at 14:39):

Yes, we can check that, or at least that it's applied to something that's not an inductive type.

#### Rob Lewis (Sep 30 2019 at 14:42):

All of the current derive handlers apply only to inductives. delta_instance applies only to defs. So this is safe until we think of another handler we want to apply to defs.

#### Rob Lewis (Sep 30 2019 at 14:43):

It does seem a little hackish, but it also feels a little bad to use two attributes @[derive ...] for inductives and @[derive_inst ...] for defs.

#### Keeley Hoek (Sep 30 2019 at 14:47):

It seems like the derive system will always have trouble whenever there are two different ways of deriving the same class (unless you're happy with never ever getting error messages for one of the classes)

Last updated: May 10 2021 at 23:11 UTC