Dependent typed power

Stream: Is there code for X?

[Alfredo Moreira-Rosa]

So for my dimensional analysis library, i needed dependent typed powers, indeed, the dimension of quantity kg^2 is Mass^2 and has type Quantity Mass^2 Real.

So using Typeclasses does not not allow to have a generic dependant power function.

I created a new notation with a custom elaborator, i share it here in case it can be of some help :

/--
Dependent power operator, allows to have the output type depend on the exponent.
`q ^ᵈ n`:
- if `n : ℕ` uses `q.npow`
- if `n : ℤ` uses `q.zpow`
- if `n : ℚ` uses `q.qpow`

Examples:
- `q ^ᵈ 2`          -- npow
- `q ^ᵈ (-2 : ℤ)`   -- zpow
- `q ^ᵈ (1/3 : ℚ)`  -- qpow
-/
syntax:80 (name := dependentPow) term:80 " ^ᵈ " term:81 : term

elab_rules : term
  | `($q:term ^ᵈ $n:term) => do
      let ne ← elabTerm n none
      let nty ← whnf (← inferType ne)

      let makeDot (field : Name) : TermElabM (Expr) := do
        let stx ← `(($q).$(mkIdent field) $n)
        elabTerm stx none

      match nty with
      | .const ``Nat _ => makeDot `npow
      | .const ``Int _ => makeDot `zpow
      | .const ``Rat _ => makeDot `qpow
      | _ => throwErrorAt n m!"exponent must be ℕ, ℤ, or ℚ; got type {nty}"

and here an exemple of defined power instances for Nat, Int and Rat :

def npow [Pow α ℕ] (q : Quantity d α) (n : ℕ) : Quantity (n•d) α :=
    { val := q.val ^ n }

def zpow [Pow α ℤ] (q : Quantity d α) (n : ℤ) : Quantity (n•d) α :=
    { val := q.val ^ n }

def qpow [Pow α ℚ] [SMul ℚ δ] (q : Quantity d α) (n : ℚ) : Quantity (n•d) α :=
    { val := q.val ^ n }

[Notification Bot]

This topic was moved here from #Is there code for X? > Dependant type power by ecyrbe.

[Eric Wieser]

A custom elaborator is probably unnecessary here, you could just create a DPow typeclass for dependent powers

[Eric Wieser]

(there are previous threads which do this)

[Alfredo Moreira-Rosa]

i did not find any, any pointers ?

[Alfredo Moreira-Rosa]

By the way, i tried something like this, and it did not work as i wanted and required extra work in proofs (because Out n is not reduced).

class DPow (α : Type u) (γ : Type v) where
  Out : γ → Type w
  pow : (q : α) → (n : γ) → Out n


infix:80 (priority := high) " ^ᵈ " => DPow.pow

[Alfredo Moreira-Rosa]

With the elaborator solution, everything was as if i wrote q.npow manually, not the case with typeclasses

[Eric Wieser]

You're looking for

class DPow (α : Type u) (γ : Type v) (Out : outParam (γ → Type w_)) where
  pow : (q : α) → (n : γ) → Out n


infix:80 (priority := high) " ^ᵈ " => DPow.pow

i think

[Eric Wieser]

ecyrbe said:

i did not find any, any pointers ?

#new members > Type classes and dependent types @ 💬

[Alfredo Moreira-Rosa]

i always forget about outParam... thanks