inferInstance v infer_instance

Stream: lean4

[Kevin Buzzard]

The tactic rfl is now spelt the same as the term rfl and I think historically we have plenty of justification for the claim that this is less confusing for beginners (there are several examples on this Zulip of people asking what the difference is between rfl and refl in Lean 3). Similarly the tactic sorry and the term sorry are spelt the same. Would it be a good idea to hence unify the spelling of the term inferInstance and the tactic infer_instance? This just came up in my teaching.

[Henrik Böving]

In principle: Since it has an underscore/two words this would go against our typical name scheme of snek case for tactics and proof stuff and camel case for proper values. I don't know if it is reasonable to make an exception here? If we do make an exception we should make it consistent, i.e. every term that has a corresponding tactic should be named the same style.

[Geoffrey Irving]

instance?

[Henrik Böving]

That's a keyword, not such a good idea

[Damiano Testa]

inst?

[Jireh Loreaux]

inst is frequently used as a variable name, so I'm not a fan of changing to that.

[Eric Wieser]

I think this is a nice lesson in "tactics use a different naming convention to definitions", and everything is working as intended

[Yury G. Kudryashov]

If you want to allow both spellings in your course or local repository, then it's easy to do.

[Mario Carneiro]

I think it would be better if they were called synth_instance. It is confusing that the command is called #synth but I can never remember if the tactic is called infer_instance or apply_instance or synth_instance

[Mario Carneiro]

(or conversely I suppose we could rename the other command to #infer)

[Mario Carneiro]

Come to think of it, synth could probably be used alone, without the "instance" part, resulting in a synth term/tactic and #synth command

[David Thrane Christiansen]

It certainly makes sense to use consistent terminology for operations. Is "synthesis" the appropriate thing to be consistent with?

As far as I know, no other system uses this terminology. Coq calls it "inference", while Haskell and Agda call it "resolution". Usually, I would expect synthesis to be something done either in the tradition of bidirectional type checking or in the field of program synthesis, which is not really the heritage of this feature.

[Henrik Böving]

The original reason for synthesis to surface to the user is probably that it is internally refererred to as synthesis as well, you have e.g. synthInstance tracing etc.

[Mario Carneiro]

Considering the abstract (CS) meanings of "synthesis" and "inference", I think that typeclass inference leans much more on the "synthesis" side than "inference" - it's constructing a term not by unification but by sticking pieces together in ~arbitrary order, with non-unique results which don't really resemble any of the inputs directly. IMO it's not too far from program synthesis

[Mario Carneiro]

Lean does "inference", when it infers _ in terms by unification. Seems like a good idea to keep this concept distinct from the exploratory thing that is typeclass inference

[Johan Commelin]

So should we start calling it "typeclass synthesis" instead?

[Eric Wieser]

So synthInstance and synth_instance?

[Mario Carneiro]

or just synth as I mentioned above

[Jireh Loreaux]

Just synth I think is nice, and I like the distinction between instance synthesis and inference of holes.