Idiomatic Instance Declarations

Stream: new members

[Mark Fischer]

In mathlib, I've noticed that instance declarations often tend to just call separately defined functions. So instead of

instance instFooString : ToString Foo where
    toString _ := "Bar"

I see something like:

def Foo.toString (_ : Foo) : String := "Bar"

instance instFooString : ToString Foo where
    toString := Foo.toString

---

It seems like these should be roughly equivalent. Is there a pragmatic reason beyond style to prefer one over the other? My only guess is that you can save the compiler a Typeclass lookup when you write something like f.toString to call the function directly.

[Eric Wieser]

Usually the first one is preferrable in mathlib

[Eric Wieser]

If you write the second one, you then need to write a lemma that says Foo.toString f = toString f

[Eric Wieser]

My only guess is that you can save the compiler a Typeclass lookup when you write something like f.toString to call the function directly.

This is a false economy because now you have a spelling of toString that there are no theorems about!

[Eric Wieser]

(though toString is a bad example; think Nat.mul m n vs m * n)

[Mark Fischer]

Nat.mul seems to follow the second style?

[Mark Fischer]

Or like:

def Nat.lt (n m : Nat) : Prop :=
  Nat.le (succ n) m

instance : LT Nat where
  lt := Nat.lt

instead of

instance : LT Nat where
  lt n m := Nat.le (succ n) m

[Eric Rodriguez]

Treq said:

Nat.mul seems to follow the second style?

Yes, Eric is saying that it doesn't have many theorems proved about it in the form Nat.mul a b, so it's awkward to work with.

[Mark Fischer]

Right. Okay, I follow

[Kyle Miller]

There's a pragmatic reason in the generated code: the compiler usually inlines instance definitions, so having a separate definition prevents the compiler from inlining the main definition. If the definition is complicated, like a big match expression, this can save a lot on compilation time. I had one case that improved the compilation time by around 10x if I remember correctly.

[Kyle Miller]

With Nat.mul and the like, one reason I believe is to have a definition that the kernel can know the name of, since it contains code to accelerate the computation using a bignum library, rather than by evaluating it by the Lean definition.

[Mark Fischer]

I think my takeaway is this: I should expect to see both styles in wild. I should prefer the first style unless I have pragmatic reasons to move to the second.

[Mario Carneiro]

Another reason to use an instance that points at a definition is that at "instance reducibility", used by instance search, it will unfold instances but not regular definitions. So if you have a big and complicated definition then this trick will avoid it getting unfolded during instance search. This is usually a good idea once you get past the "record containing more records" stage.