Zulip Chat Archive

Stream: general

Topic: Bad instance name lint


view this post on Zulip Mario Carneiro (Aug 12 2020 at 18:15):

This has caught me out many times, so I'm wondering if we can get a lint to watch for it (or maybe even fix lean so it doesn't happen).

inductive widget : Type
inductive doodad : Type

instance : has_to_string widget := ⟨λ x, by cases x -- widget.has_to_string
instance : has_to_string doodad := ⟨λ x, by cases x -- doodad.has_to_string

namespace foo

inductive widget : Type
inductive doodad : Type

instance : has_to_string widget := ⟨λ x, by cases x -- foo.has_to_string
instance : has_to_string doodad := ⟨λ x, by cases x -- foo.has_to_string, error

end foo

Usually I won't even notice that foo.widget's instance has a name that doesn't mention widget until I write foo.doodad and hit the name conflict, so I'm quite sure that there are many uncaught instances of this problem in mathlib.

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 18:23):

ha ha I'm not sure I want to know the number of instances with bad names in mathlib :-) Wouldn't it be more fun to change Lean so that it names the instances in a cleverer way and then see if mathlib still compiles? So what is the algorithm for naming instances? It's well-known that the current method is laughed at but is there a cleverer proposal which is less bad? In namespace foo I decide to prove foo A -> baz B -> bar (prod A B) and also bar A -> foo B -> baz (prod A B) (with foo, bar, baz all classes). Are these now both named something like foo.prod? What is your proposal for the example you post? What do you want has_to_string foo to be called in namespace foo? I think there was a discussion here a long time ago about naming lemmas and how it wasn't at all automatic because you have a tree of constants which you want to turn into a list of constants.

view this post on Zulip Mario Carneiro (Aug 12 2020 at 18:57):

I think that for the most part the instance names that are automatically generated are okay, not great but usable

view this post on Zulip Mario Carneiro (Aug 12 2020 at 18:58):

not to mention that they more or less by necessity have to define our style guide for naming instances

view this post on Zulip Mario Carneiro (Aug 12 2020 at 19:01):

I think that the right answer in this instance is that namespaces should always just append, never replace bits of the name. So this one should be called foo.widget.has_to_string

view this post on Zulip Mario Carneiro (Aug 12 2020 at 19:02):

Although, I think that this would name your instances foo.prod.bar and foo.prod.baz respectively which is a bit odd to say the least

view this post on Zulip Mario Carneiro (Aug 12 2020 at 19:05):

Another thing that would help is if the instance naming algorithm was more comfortable saying "I don't know what to call this, you do it"

view this post on Zulip Mario Carneiro (Aug 12 2020 at 19:07):

For example

instance : has_to_string (Sort -> Sort) := sorry

gives failed to synthesize instance name, name should be provided explicitly but

namespace foo
instance : has_to_string (Sort -> Sort) := sorry
end foo

gives foo.has_to_string like the others. I think that when this situation occurs (lean wants to call it foo.has_to_string) we are in the case that we should at least lint and maybe also give the failed to synthesize instance name error

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 19:13):

I think I'd rather be asked for an instance name than accidentally name an instance badly

view this post on Zulip Mario Carneiro (Aug 12 2020 at 19:17):

Here is the relevant code:

        /* Try to synthesize name */
        expr it = type;
        while (is_pi(it)) it = binding_body(it);
        expr const & C = get_app_fn(it);
        name ns = get_namespace(p.env());
        if (is_constant(C) && !ns.is_anonymous()) {
            c_name = const_name(C);
            scope.set_name(c_name);
        } else if (is_constant(C) && is_app(it) && is_constant(get_app_fn(app_arg(it)))) {
            c_name = const_name(get_app_fn(app_arg(it))) + const_name(C);
            scope.set_name(c_name);
        } else {
            p.maybe_throw_error({"failed to synthesize instance name, name should be provided explicitly", c_pos});
            c_name = mk_unused_name(p.env(), "_inst");
        }

In english, it says to get the conclusion of the theorem, and call it it, with the head constant of it (the instance like has_to_string) being C. If we are not at the top level, then name it current_namespace.C (this is the bad case), else if the last argument of it is itself a constant D applied to things then name it current_namespace.D.C, else complain to the user

view this post on Zulip Mario Carneiro (Aug 12 2020 at 19:19):

We could just swap the two if statements, so that the present case gets the name current_namespace.D.C, and the scheme current_namespace.C is only used for things like the has_to_string (Sort -> Sort) example

view this post on Zulip Mario Carneiro (Aug 12 2020 at 19:19):

or we could just delete that case entirely so that this case gives the failed to synthesize instance name error

view this post on Zulip Reid Barton (Aug 29 2020 at 16:48):

I think the first case probably exists to handle situations like

structure foo : Type
namespace foo
instance : has_add foo := ⟨λ _ _, ⟨⟩⟩
end foo
#check foo.has_add   -- not `foo.foo.has_add`

because it's pretty common to create a structure and then add a lot of things in a namespace, and some of those things are likely to be instances for the structure you just made.

view this post on Zulip Reid Barton (Aug 29 2020 at 16:50):

Of course it can also choose the wrong name in other situations, for example if the namespace is something like category_theory

view this post on Zulip Reid Barton (Aug 29 2020 at 16:55):

How about this heuristic: drop the first case and, in the second case, don't include the D part of the name if it equals the last component of the current namespace.

view this post on Zulip Reid Barton (Aug 29 2020 at 17:56):

A better version of this is: drop the current namespace from either the C or the D component if it happens to be a prefix of them

view this post on Zulip Reid Barton (Aug 29 2020 at 20:50):

lean#458 is my proposal

view this post on Zulip Reid Barton (Aug 30 2020 at 00:39):

wait, no. I was supposed to say "My proposal is lean#458"


Last updated: May 10 2021 at 00:31 UTC