Stream: new members
Topic: choose typeclass instance
Aron Fischer (Apr 14 2021 at 13:34):
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 (Apr 14 2021 at 13:37):
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 (Apr 14 2021 at 13:40):
outParam means the following: If you see
a * b, then you can figure out the type of
b, let's call them
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 * b will have type
Aron Fischer (Apr 14 2021 at 13:41):
Typeclasses are supposed to have a unique solution, not counting outParams
good to know. thanks
Important: this should have a unique solution
Last updated: May 11 2021 at 13:22 UTC