instance of `HPow Float Nat` doesn't exist

Stream: general

[Asei Inoue]

why?

variable (f : Float) (n : Nat)

#check_failure f ^ n

[Asei Inoue]

spinylobster suggest to add a following code. How about this?

instance [∀ n, OfNat α n] [HPow α α α] : HPow α Nat α where
  hPow x n := x ^ (OfNat.ofNat n : α)

#eval 0.1 ^ 2

[Julian Berman]

Doesn't that #evalwork even without the instance? Specifically it looks like there already is an OfNat for Float.

[Julian Berman]

I don't really know what the norms are but I guess I'm slightly surprised (in a "I don't know what I'm doing so probably there's a reason but I wouldn't have guessed this" sense) that 1) HPow doesn't look for a coercion instance and use it in general and 2) there actually is no coercion instance from Nat to Float (besides the OfNat there's Nat.toFloat but it's not a Coe. That coercion is lossy obviously, so maybe that's the reason it's not marked Coe, or maybe that just wasn't useful for anything, or...)

[Eric Wieser]

That use of OfNat isn't legal, you're only supposed to use it for numeric literals

[Eric Wieser]

It surpriseds me that we have both docs#Nat.toFloat and docs#Float.ofNat

[Julian Berman]

The former is just an alias, yeah? Maybe just for discoverability?

[Asei Inoue]

@Eric Wieser You say this is not legal?

#check_failure f ^ n

instance [∀ n, OfNat α n] [HPow α α α] : HPow α Nat α where
  hPow x n := x ^ (OfNat.ofNat n : α)

#check f ^ n

[Julian Berman]

I thought Eric was right too but I see some other instances where OfNat _ n n is not some honest-to-goodness natural number literal?

[Julian Berman]

E.g. core has... instance : OfNat JsonNumber n := ⟨JsonNumber.fromNat n⟩

[Julian Berman]

And a few others which are very similar it looks like?

[Julian Berman]

Oh right and the OfNat for Float itself of course... instance : OfNat Float n := ⟨Float.ofNat n⟩

[Julian Berman]

Oh sorry, but I misunderstood Eric's message, yeah, that was similar to what I was trying to say too by pointing out the instance you defined isn't needed. Basically OfNat is only if you're going to write ^ 2, not if you have ^ n and n is a variable.

[Asei Inoue]

Basically OfNat is _only_ if you're going to write ^ 2, not if you have ^ n and n is a variable.

I see. I understand the meaning of the message.

[Asei Inoue]

Ok this works.

variable (f : Float) (n : Nat)

#check_failure f ^ n

instance : HPow Float Nat Float where
  hPow a b := a ^ b.toFloat

#check f ^ n

My point was why this instance is not included in Std or Mathlib.

[Eric Wieser]

I think you're supposed to work with floats everywhere in the first place

[Eric Wieser]

Mixing infinite precision nats and lossy floats is a bit weird

[Yury G. Kudryashov]

The generic instance above will create a diamond, e.g., for Real. As for Float, one may want to have an instance implemented in C/C++ that uses nat-specific pow in case the number is not a long number.

[Yury G. Kudryashov]

Or should it work with types like UInt64 instead?

[Kyle Miller]

Elaboration for ^ is fiddly, and you have to be very careful with global instances. The issue is that we're trying to make it so that when, for example, x y : Real, then x ^ 2 gives the HPow Real Nat Real instance but x ^ y gives the HPow Real Real Real instance.

Regarding Float instances, I just made sure that the homogeneous Pow Float instance worked.

I don't see a problem with including that specific HPow Float Nat Float instance. You just have to be aware that (3 : Float) ^ 2 will still elaborate with 2 : Float.