typeclass or implicit arguments

Stream: general

[Sebastien Gouezel]

I keep coming back to the question of typeclass or implicit arguments, as I feel I still don't understand well enough what is going on. Let me take the example of the continuity of composition for the sake of the discussion. In mathlib, we have

#print continuous.comp
theorem continuous.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [_inst_1 : topological_space α] [_inst_2 : topological_space β]
[_inst_3 : topological_space γ] {g : β → γ} {f : α → β}, continuous g → continuous f → continuous (g ∘ f)

#print continuous
def continuous : Π {α : Type u_1} {β : Type u_2} [_inst_1 : topological_space α] [_inst_2 : topological_space β],
  (α → β) → Prop

In continuous.comp, the explicit arguments continuous g and continuous f already contain information about some topologies. So, when we use continuous.comp, instance search fires to find topologies on α, β and γ, and then it sees the arguments continuous g and continuous f and it checks that the topologies found by instance search are defeq to the ones in these arguments.

If instead the topologies in continuous.comp where implicit arguments, then none of this would be needed. However, this is not what we do usually, so I was afraid of some trap. As a little experiment, I changed the definition of continuous.comp to have

theorem continuous.comp : ∀ {α : Type u} {β : Type v} {γ : Type w} {hα : topological_space α} {hβ : topological_space β}
{hγ : topological_space γ} {g : β → γ} {f : α → β}, continuous g → continuous f → continuous (g ∘ f)

Surprisingly, mathlib compiles perfectly well with this change (and I know that continuous.comp is used zillions of times, so this should be a robust check).

Is there any drawback to this, or should we change our practice and change typeclass argument to implicit arguments whenever this is possible? (And I have the impression this would be possible at many many many places!)

[Kevin Buzzard]

However, this is not what we do usually, so I was afraid of some trap

Isn't this because we had got into our habits before Chris' brilliant idea?

[Sebastien Gouezel]

Probably yes, but I had not realized yet how this is applicable all over mathlib. Would this be lintable?

[Sebastien Gouezel]

An issue is that it would be cumbersome to adjust the (typeclass or implicit) parameters to each statement. Ideally, one could declare parameters with variable {[topological_space α]}, meaning use typeclass unless this is inferrable from later parameters. But this looks like science-fiction to me.

[Mario Carneiro]

The reason it works in this case is because continuous f and continuous g are hypotheses, which then determine these arguments. Often, the arguments are determined by the type of the conclusion instead, in which case this trick doesn't work. Basically it's the same rule as when we ask if an argument should be implicit vs explicit, except here it is implicit vs instance implicit

[Mario Carneiro]

The science fiction solution is actually fact for binder inference in projections of structures; this is the reason why things list.nil would have an explicit alpha but list.cons doesn't (except that we override this behavior in that particular case with the funny | nil {} : list notation)

[Sebastien Gouezel]

Sure, you need a hypothesis (Prop or Type) determining the typeclass. But this happens everywhere! I just opened a file at random and took a random statement:

theorem minimal_polynomial.min : ∀ {α : Type u} {β : Type v} [_inst_1 : comm_ring α] [_inst_2 : comm_ring β] [_inst_3 : algebra α β] {x : β}
(hx : is_integral α x) {p : polynomial α},
  polynomial.monic p → ⇑(polynomial.aeval α β x) p = 0 → degree (minimal_polynomial hx) ≤ degree p

All the typeclass arguments can be made implicit as they are already contained in is_integral α x.

[Sebastien Gouezel]

I can see several options here.
1) Don't change anything to our practice
2) In new additions, make implicit the parameters that can be made implicit, and also do it in existing files when it seems useful (possibly with the help of a linter)
3) Wait for Lean 4, and build there a mechanism that will transform automagically typeclass arguments into implicit arguments if they can be inferred from a later argument.
4) (unrealistic) fix everything in mathlib

Any opinion about this? I think it is an important question for performance in Lean 3 as instance search is often a bottleneck.

[Kevin Buzzard]

4) (unrealistic) fix everything in mathlib

It's the regex challenge!

[Mario Carneiro]

I don't think this is actually a performance problem, because you still have to search for the instance the first time (in the is_integral α x argument for example) and later searches should just hit the cache. But it does solve the issue with unified instances not matching inferred

[Scott Morrison]

Is it so unrealistic to fix everything in mathlib? Especially if we can get some linter help, it can be done incrementally.