Zulip Chat Archive

Stream: general

Topic: has_pow


view this post on Zulip Andrew Ashworth (Mar 31 2018 at 07:20):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Sebastian Ullrich (Apr 02 2018 at 09:38):

@Mario Carneiro Hmm, this is certainly unexpected

view this post on Zulip 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.

view this post on Zulip Sebastian Ullrich (Apr 02 2018 at 21:51):

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

view this post on Zulip 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.

view this post on Zulip Sebastian Ullrich (Apr 03 2018 at 09:06):

Okay, I'll remove it


Last updated: May 13 2021 at 05:21 UTC