Zulip Chat Archive

Stream: general

Topic: type class instances of superclasses


view this post on Zulip Sean Leather (Jun 21 2018 at 12:08):

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?

view this post on Zulip Mario Carneiro (Jun 21 2018 at 12:09):

Depends on what you mean by "automatically get"

view this post on Zulip Mario Carneiro (Jun 21 2018 at 12:10):

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

view this post on Zulip Sean Leather (Jun 21 2018 at 12:10):

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

view this post on Zulip Sean Leather (Jun 21 2018 at 12:13):

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?

view this post on Zulip Mario Carneiro (Jun 21 2018 at 12:14):

yes

view this post on Zulip Sean Leather (Jun 21 2018 at 12:15):

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”?

view this post on Zulip Mario Carneiro (Jun 21 2018 at 12:16):

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

view this post on Zulip Sean Leather (Jun 21 2018 at 12:19):

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

view this post on Zulip Mario Carneiro (Jun 21 2018 at 12:22):

B.to_A I believe

view this post on Zulip Sean Leather (Jun 21 2018 at 12:28):

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

view this post on Zulip Sean Leather (Jun 21 2018 at 12:29):

#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 α)

view this post on Zulip Sean Leather (Jun 21 2018 at 12:30):

Lots of lattice.lattice.

view this post on Zulip Sean Leather (Jun 21 2018 at 12:31):

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 α

view this post on Zulip Sean Leather (Jun 21 2018 at 12:33):

Thanks, Mario!

view this post on Zulip Sean Leather (Jun 21 2018 at 12:36):

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 α

view this post on Zulip Mario Carneiro (Jun 21 2018 at 12:55):

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

view this post on Zulip Sean Leather (Jun 21 2018 at 13:06):

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 α)).

view this post on Zulip Sean Leather (Jun 21 2018 at 13:10):

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).

view this post on Zulip Simon Hudon (Jun 21 2018 at 18:00):

Do you know about #print instances?

view this post on Zulip Sean Leather (Jun 22 2018 at 06:43):

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

view this post on Zulip Simon Hudon (Jun 22 2018 at 15:00):

oops! Sorry!


Last updated: May 13 2021 at 18:26 UTC