## Stream: general

### Topic: has_pow

#### Andrew Ashworth (Mar 31 2018 at 07:20):

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

#### Mario Carneiro (Mar 31 2018 at 07:49):

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 (Mar 31 2018 at 09:20):

@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 (Apr 02 2018 at 02:33):

@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 (Apr 02 2018 at 02:35):

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

#### Mario Carneiro (Apr 02 2018 at 09:28):

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 (Apr 02 2018 at 09:38):

@Mario Carneiro Hmm, this is certainly unexpected

#### Sebastian Ullrich (Apr 02 2018 at 21:38):

@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 (Apr 02 2018 at 21:51):

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

#### Mario Carneiro (Apr 02 2018 at 23:16):

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 (Apr 03 2018 at 09:06):

Okay, I'll remove it

Last updated: May 13 2021 at 05:21 UTC