has_pow

Stream: general

[Andrew Ashworth]

what's the impact of the new has_pow typeclass being an out_param?

[Mario Carneiro]

I'm not sure about this change. Sebastian suggested it and it was merged before we had much discussion about it, but I don't know if it's reasonable. mathlib already had and discarded an earlier typeclass proposal. In particular, the reals are going to have at least three power operations on them, and it's not clear to me how to disambiguate the typeclass search

[Sebastian Ullrich]

@Mario Carneiro Would that be monoid_pow/group_pow/real_pow (or whatever class that last one is defined on)? Since each one is strictly more general in its out_param type than the ones before it, would it make sense to give them increasing instance priorities?

[Mario Carneiro]

@Sebastian Ullrich I've started working on fixing mathlib after the has_pow change. Here's an example of a problem that arises:

variables {α : Type*} [group α]
def gpow : α → ℤ → α := sorry
instance group.has_pow : has_pow α ℤ := ⟨gpow⟩

example (a : α) : a ^ 0 = 1 := sorry -- failed to synth ⊢ has_pow α ℕ
example (a : α) : a ^ (0:ℕ) = 1 := sorry -- ok, coerces
example (a : α) : a ^ (0:ℤ) = 1 := sorry -- ok

[Mario Carneiro]

Do out_params not propagate type information to the arguments for the purpose of avoiding the nat default for number literals?

[Mario Carneiro]

Okay, this update isn't going to happen today, I need to sleep. The change is generally making me put in more type ascriptions than before, but it wasn't disambiguating anything before so maybe that's reasonable. It's not going to be fun explaining why this happens though

[Sebastian Ullrich]

@Mario Carneiro Hmm, this is certainly unexpected

[Sebastian Ullrich]

@Mario Carneiro Okay, it's unfortunate scheduling between the class inference and the coercion, which I don't think is a perfectly solvable problem in general. I don't know if we can do a better job for this common case, hmm.

[Sebastian Ullrich]

Would you suggest to just remove the out_param (for now)?

[Mario Carneiro]

My gut says that will perform better on the whole. We will have to give the type of things in that slot if they aren't derivable normally, but this will give more freedom to have multiple possibly incompatible power functions which are selected by type. I'll finish updating mathlib wrt the current version, and then if you change it to remove the out_param and I fix mathlib again we will have a basis for comparison.

[Sebastian Ullrich]

Okay, I'll remove it