deriving instances

Stream: general

[Johan Commelin]

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]

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]

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

[Scott Morrison]

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

[Rob Lewis]

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]

Awesome! Thanks for starting this.

[Scott Morrison]

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]

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

[Rob Lewis]

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

[Johan Commelin]

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]

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]

local attribute [reducible] power_series?

[Sebastien Gouezel]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Rob Lewis]

#1475

[Johan Commelin]

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

[Scott Morrison]

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

@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]

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].

[Scott Morrison]

oh ... :-)

[Scott Morrison]

Maybe there is very little payoff at all, sorry.

[Floris van Doorn]

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

@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]

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]

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

[Rob Lewis]

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]

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]

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]

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

[Reid Barton]

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]

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]

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]

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]

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]

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]

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

[Rob Lewis]

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]

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

[Rob Lewis]

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]

Priority first, most recent secondary

[Rob Lewis]

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

[Sebastian Ullrich]

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]

Is the recently added simps an example?

[Johan Commelin]

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

[Reid Barton]

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]

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

@[derive decidable_eq] def S := ℕ

[Reid Barton]

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]

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]

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]

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

[Rob Lewis]

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]

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]

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)