choose typeclass instance

Stream: new members

[Aron Fischer]

Hi,
I am just learning lean 4 syntax from the docs.
I am in the chapter on Typeclasses and Default Instances of https://leanprover.github.io/lean4/doc/typeclass.html

I was trying to understand the outParam keyword and why it is needed, and I also was experimenting with having two different versions of hMul that differ only in the outParam. One for Nat Nat Nat and one for Nat Nat Int.

       -- start with my own version of HMul
      class HMul' (α : Type u) (β : Type v) (γ : outParam (Type w)) where
        hMul : α → β → γ

      -- Mulitplication Nat Nat Nat as ususal
      instance : HMul' Nat Nat Nat where
        hMul := Nat.mul

      -- With a weird one for Nat Nat Int.
      @[defaultInstance]
      instance : HMul' Nat Nat Int where
        hMul x y := -3

      -- This uses the default instance as expected
      #eval HMul'.hMul 4 5
       -- -3

      --
      -- but how do I specify when I want the other one?
      -- If I do
      #check @HMul'.hMul Nat Nat Nat _ 3 4
        -- failed to synthesize instance HMul' Nat Nat Nat
       -- and if I do
       #check @HMul'.hMul Nat Nat Nat Nat.mul 3 4
       -- I get
       -- argument  Nat.mul has type Nat → Nat → Nat : Type but is expected to have type  HMul' Nat Nat Nat : Type
       -- How do I choose the typeclass instance I want?

[Mario Carneiro]

Typeclasses are supposed to have a unique solution, not counting outParams. So those two instances are conflicting, and you will only ever get one of them (determined by the priority on the instances, or the declaration order). The other one can only be accessed via @, so it's not recommended to do this at all.

[Johan Commelin]

@Aron Fischer outParam means the following: If you see a * b, then you can figure out the type of a and b, let's call them A and B. Now search for an instance HMul' A B ???.

Important: this should have a unique solution. In particular, the ??? will be filled in by some type C that should be uniquely determined by A and B.

Result: a * b will have type C.

[Aron Fischer]

Typeclasses are supposed to have a unique solution, not counting outParams

good to know. thanks

Important: this should have a unique solution

:+1: