Type classes and dependent types

Stream: new members

[Alexander Niederbühl]

Let's say I have the following:

structure Quantity (dimension: Dimension) where
  val: Float
deriving Repr

structure Dimension where
  val: Int := 1

instance : HPow Dimension Int Dimension where
  hPow d power := {
    val := d.val * power
  }

Is it possible to define the exponentation of Quantity by Int such that
the value of the Int is used in the type of the output parameter?

Something like along the lines of:

instance {d: Dimension} : HPow (Quantity d) Int (Quantity (d^power)) where
  hPow quantity power :=  { val := quantity.val^(Float.ofInt power)}

or

instance {d d': Dimension} : HPow (Quantity d) Int (Quantity d') where
  hPow quantity power :=  { val := quantity.val^(Float.ofInt power) : (Quantity (d^power))}

?

[Eric Wieser]

Unfortunately I don't think this is possible with the design of HPow, but you could write a custom HPowDep typeclass

[Eric Wieser]

docs#GradedMonoid.GMonoid.gnpow is pretty much what you want I think

[Alexander Niederbühl]

Eric Wieser said:

docs#GradedMonoid.GMonoid.gnpow is pretty much what you want I think

Thanks, but I'm really lost on how to apply this to the problem. Could you give me an example?

[Eric Wieser]

Looking more closely that doesn't work for you out of the box; quantities are a multiplicatively-gtaded monoid but mathlib only has the additive case

[Eric Wieser]

The link would be to show GradedMonoid.GMonoid (fun d : Additive Dimension => Quantity (Additive.toMul d), which might be an interesting exercise but probably won't help you much

[Alexander Niederbühl]

Ok, how about the approach to write a custom HPowDep, would this be more viable?

[Eric Wieser]

That would certainly work for your use case, and should be straightforward

[Eric Wieser]

Persuading Lean corr to adopt that typeclass might be slightly harder!

[Alexander Niederbühl]

Eric Wieser said:

That would certainly work for your use case, and should be straightforward

I'm sorry these are my first lines of lean code and I'm completely lost at how that would look like.

[Eric Wieser]

It would look something like

class HPowDep (α β : Type*) (γ : β → Type*) where
  hPow (a : α) (b : β) : γ b

infixr:80 " ^ " => HPowDep.hPow

[Eric Wieser]

Then you can provide a instance : HPowDep (Quantity d) Int (fun power => Quantity (d^power)) instance

[Alexander Niederbühl]

This is a good starting point for me, thanks!