Requesting clarification about instances

Stream: lean4

[Soham Saha]

#check sizeOf_default (α:=Nat) 5
#check sizeOf_nat 5

In the infoview, the respective types shown are sizeOf 5 = 0 and sizeOf 5 = 5.

On hovering, the sizeOf functions are further clarified to be @sizeOf Nat (instSizeOfDefault Nat) and @sizeOf Nat instSizeOfNat 5.

This happens because Nat has been raised to the SizeOf typeclass in two different ways (see lines 52 to 60 here).

Now, I have a few questions about this:

(i) I thought previously that it should not be possible to raise a type to a typeclass via two different instantiations, and would have expected the instSizeOfNat to override the low-priority default instantiation. Is it because the default definition here has a theorem associated with it which makes it stick around even after being overriden?

(ii) Are type classes essentially equal to type constructors? I feel there must be some semblance between them since raising a type to a typeclass via two different means have different objects associated to them (in this case instSizeOfDefault Nat and instSizeOfNat), which seems (to me) as if SizeOf is internally represented as a type constructor, and type classes are just syntactic sugar.

(iii) Is there anything better than #check for general use which highlights this instance distinctions? To clarify the context, I generally use #check for checking types, but I was thoroughly confused when I saw this multiple instance thingy happen in something else I was trying to prove. It took me quite a long time to realize that they were two different sizeOfs that were being used.

[Also, I am not quite sure if this would be better suited on general, if so, please tell and I will shift this discussion there]

[Mirek Olšák]

(i) Notice that both sizeOf_default, and sizeOf_nat do not have any typeclass assumptions in their type. Hence, you are not triggering any typeclass search when calling these #check. The search was already done when the theorems were defined, you can do just #check sizeOf_default, and hovering over sizeOf will show you that this theorem uses the instSizeOfDefault instance no matter which type you plug in.

(ii) You should think of class just as a structure with some default instances. These instances get automatically filled at the moment when a constant with a typeclass arguments is applied. The exact rules are generally loose, so it could happen that you get a typeclass conflict.

(iii) You can run

#synth SizeOf Nat -- full typeclass search
#instances SizeOf Nat -- single search step, requires at least `import Batteries`

[Soham Saha]

@Mirek Olšák Thank you very much for your answer.

However, I am still a bit confused about (ii). Isn't the key idea of using type classes (instead of using type constructors) that we are supposed to have only one instance declaration for raising a given type to some particular typeclass? (as discussed here). But here, multiple instance declarations have their own objects, and SizeOf seems to be behaving like a type constructor (since we have instSizeOfNat : SizeOf Nat and instSizeOfDefault Nat : SizeOf Nat). What is the reason/ design decision behind having multiple instance declarations for a given type? And are typeclasses internally implemented as type constructors?

[Mirek Olšák]

I would not take haskell as a ground truth because it works a bit differently from Lean. The main idea of using typeclasses is that they get inferred automatically, not about uniqueness.

Of course, we don't want typeclass conflicts to happen in practice, so we are trying to have (up to defeq) uniquelly assigned typeclass instances but there is no theoretical obligation to do so, and in some cases (like SizeOf) there can be the specific instances, and a low-priority backup instance.

[Mirek Olšák]

By the way, as I am planning to teach Lean, here is my write-up about typeclasses. I am discussing typeclass conflicts there on lines 267 -- 300. (haven't tested on students yet, so feedback welcome)

[Soham Saha]

@Mirek Olšák Thanks for the clarification about typeclasses and they being inferred automatically, it did clear things up. Also, thanks for the example code in the write-up! :+1: