Zulip Chat Archive

Stream: general

Topic: deriving instances


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

view this post on Zulip 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 `AT/s` := r.top_loc

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

instance : comm_ring AT/s := by find_inst

instance : module A AT/s := by find_inst

instance : algebra A AT/s := by find_inst

view this post on Zulip Sebastian Ullrich (Aug 27 2019 at 07:51):

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

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

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

view this post on Zulip Johan Commelin (Aug 27 2019 at 08:23):

Awesome! Thanks for starting this.

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

view this post on Zulip Rob Lewis (Aug 27 2019 at 08:23):

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

view this post on Zulip Rob Lewis (Aug 27 2019 at 08:24):

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

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

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

view this post on Zulip Sebastien Gouezel (Sep 23 2019 at 13:29):

local attribute [reducible] power_series?

view this post on Zulip Sebastien Gouezel (Sep 23 2019 at 13:29):

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

view this post on Zulip Johan Commelin (Sep 23 2019 at 13:36):

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

view this post on Zulip Johan Commelin (Sep 23 2019 at 13:36):

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

view this post on Zulip Reid Barton (Sep 23 2019 at 13:50):

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

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

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

view this post on Zulip Rob Lewis (Sep 23 2019 at 14:18):

#1475

view this post on Zulip Johan Commelin (Sep 23 2019 at 14:22):

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

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

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

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

view this post on Zulip Scott Morrison (Sep 23 2019 at 23:56):

oh ... :-)

view this post on Zulip Scott Morrison (Sep 23 2019 at 23:57):

Maybe there is very little payoff at all, sorry.

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

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

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

view this post on Zulip Reid Barton (Sep 25 2019 at 16:30):

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

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Reid Barton (Sep 30 2019 at 14:07):

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

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

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

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

view this post on Zulip Sebastian Ullrich (Sep 30 2019 at 14:16):

Priority first, most recent secondary

view this post on Zulip Rob Lewis (Sep 30 2019 at 14:18):

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

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

view this post on Zulip Johan Commelin (Sep 30 2019 at 14:24):

Is the recently added simps an example?

view this post on Zulip Johan Commelin (Sep 30 2019 at 14:25):

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

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

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

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

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

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

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

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

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

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