type class instances of superclasses

Stream: general

[Sean Leather]

Given roughly the following combination of classes and instances:

class A (a : Type) := ...
class B (a : Type) extends B := ...
def T : Type := ...
instance : B T := ...

do you also automatically get:

instance : A T := ...

such that the latter instance is the appropriate component of the former instance?

[Mario Carneiro]

Depends on what you mean by "automatically get"

[Mario Carneiro]

typeclass inference should find it, but no additional def is made

[Sean Leather]

Let's assume I don't have a specific meaning and would welcome a precise definition of the phrase. :wink:

[Sean Leather]

typeclass inference should find it, but no additional def is made

So, if class A included a def aaa : a -> bool and you used aaa on t : T, this would use the implementation in instance : B T?

[Mario Carneiro]

yes

[Sean Leather]

Interesting. But I would not be able to explicitly reference any definition of type A T: this is what you mean by “no additional def is made”?

[Mario Carneiro]

typeclass inference would insert a term of the type BtoA BT rather than making an AT def and using that

[Sean Leather]

Okay. Does that BtoA have a name that you can #print?

[Mario Carneiro]

B.to_A I believe

[Sean Leather]

I just noticed that lattice is defined in the namespace lattice, resulting in lattice.lattice as the qualified name.

[Sean Leather]

#print instances lattice.lattice

finset.lattice.lattice : Π {α : Type u_1} [_inst_1 : decidable_eq α], lattice.lattice (finset α)
multiset.lattice.lattice : Π {α : Type u_1} [_inst_1 : decidable_eq α], lattice.lattice (multiset α)
with_zero.lattice.lattice : Π {α : Type u} [_inst_1 : lattice.lattice α], lattice.lattice (with_zero α)
with_top.lattice : Π {α : Type u} [_inst_1 : lattice.lattice α], lattice.lattice (with_top α)
with_bot.lattice : Π {α : Type u} [_inst_1 : lattice.lattice α], lattice.lattice (with_bot α)

[Sean Leather]

Lots of lattice.lattice.

[Sean Leather]

Ah, here are the conversions for lattice to semilattice_inf and semilattice_sup:

#print prefix lattice.lattice

...
lattice.lattice.to_semilattice_inf : Π (α : Type u) [s : lattice.lattice α], lattice.semilattice_inf α
lattice.lattice.to_semilattice_sup : Π (α : Type u) [s : lattice.lattice α], lattice.semilattice_sup α

[Sean Leather]

Thanks, Mario!

[Sean Leather]

I suppose the goal of this feature is to reduce the number of instances one writes. However, it does make it more difficult to determine if T is an instance of A.

#print instances lattice.semilattice_inf

lattice.semilattice_inf_bot.to_semilattice_inf : Π (α : Type u) [s : lattice.semilattice_inf_bot α], lattice.semilattice_inf α
lattice.semilattice_inf_top.to_semilattice_inf : Π (α : Type u) [s : lattice.semilattice_inf_top α], lattice.semilattice_inf α
lattice.lattice.to_semilattice_inf : Π (α : Type u) [s : lattice.lattice α], lattice.semilattice_inf α

[Mario Carneiro]

one trick for testing instance problems and getting the result is #check (by apply_instance : T A)

[Sean Leather]

That works only if A is exactly the type of the instance. For example: #check (by apply_instance : lattice.semilattice_inf (finset ℕ)) but not #check (by apply_instance : lattice.semilattice_inf (finset α)).

[Sean Leather]

Also, that's a tool for diagnosing an issue. It doesn't help discovering all the instances, which I have found to be useful in Haskell (and would find useful in Lean).

[Simon Hudon]

Do you know about #print instances?

[Sean Leather]

@Simon Hudon Did you see my uses of it above? :wink:

[Simon Hudon]

oops! Sorry!