Functions that are polymorphic over a typeclass

Stream: general

[Michael George]

I'm trying to write a function that is polymorphic across different typeclasses, and I'm having some difficulties getting it to type properly.

I'm working on interval arithmetic, and I have a structure that wraps an exact value up with a floating point approximation for that value; the type of the exact value is polymorphic:

structure FilteredReal (α : Type) where
  value : Thunk α
  approx : Float

I would like to give instances for the relevant operations that just operate pointwise on the value and approx. For example:

instance [Add \a]: Add (FilteredReal \a) where
  add x y := {
    value := Thunk.mk (fun () => x.value.get + y.value.get)
    approx := x.approx + y.approx
  }

That works fine, but I have a large number of such instances and typos are easy, and I was wondering whether I could abstract this into something like

instance [Add \a]: Add (FilteredReal \a) := \< lift Add.add \>

I tried several variations on the following to define lift:

def lift {CLS : {u : Nat} → Type u → Type u} [CLS Float]
  (op : {β : Type u} → [CLS β] → β → β → β)
  {α : Type u} [CLS α] (x y : FilteredReal α) : FilteredReal α := {
    value := Thunk.mk (fun () => op x.value.get y.value.get)
    range := op x.range y.range
  }

However, I keep having errors with universes or invalid binders or both. For example,

argument Float has type Type : Type 1 but is expected to have type Type u : Type (u + 1)

Is it possible to write something like lift?

[Chris Bailey]

I think for something like this, where the problem statement is "I need a bunch of repetitive code and it's going to be a nightmare" and not necessarily addressing some underlying structure, you probably want a metaprogram/tactic.

Universe issues aside, introducing lift and making it part of your instance's definition might not end up being totally transparent when you try to prove stuff with it later. I don't know if there's a more modern way to do this, but I wrote something in a similar vein to implement typeclasses for the fixed with integer types here, you should be able to use something very similar.

[Chris Bailey]

Just spit-balling, but something like this should work:

set_option hygiene false in
run_cmd
  for (typeName, methodName) in [(`Add, `add), ..].map (fun pr => (Lean.mkIdent pr.fst, Lean.mkIdent pr.snd)) do
  Lean.Elab.Command.elabCommand (← `(
      instance [$typeName A] : $typeName (FilteredReal A) where
        $methodName a b := {
            ..
        }
...

[Eric Wieser]

This is also a place that we could have a derive handler

[Andrés Goens]

Eric Wieser said:

This is also a place that we could have a derive handler

how difficult is that to implement directly ourselves (in user code)? is that documented somewhere?

[Marcus Rossel]

@Andrés Goens, this is an example of the scaffolding you need: https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Deriving/SizeOf.lean