Zulip Chat Archive

Stream: new members

Topic: Typeclass instantiation and extension


view this post on Zulip Kevin Sullivan (Apr 09 2021 at 16:32):

When I'm instantiating a typeclass A that extends typeclasses B and C, and when I've already instantiated B and C, to what extent can I count on Lean finding and using the B and C instances so that I don't have to provide values for their field values when specifying those of A?

view this post on Zulip Kevin Buzzard (Apr 09 2021 at 16:33):

I think you always have to put ..(show B, by apply_instance) in, even if the instance is in the type class cache.

view this post on Zulip Kevin Sullivan (Apr 09 2021 at 19:22):

Kevin Buzzard said:

I think you always have to put ..(show B, by apply_instance) in, even if the instance is in the type class cache.

Kevin B, thanks very much. Here's a piece of code that works without my saying anything about instances of superclasses (if I may use that terminology). Is it just by coincidence? If so, can you perhaps pencil in what I should have written?

class A (α : Type) := (n : nat)
class B (α : Type) := (m : nat)
class C (α : Type) extends A α, B α := (k : nat)

instance : A nat :=  1 
instance : B nat :=  2 
instance : C nat :=  3   -- works but maybe just by good luck

#reduce c                  -- {to_A := {n := 1}, to_B := {m := 2}, k := 3}

It's clear that we can't always rely on Lean finding superclass instances. And in cases where we can't, it's often unclear which or even how many fields need to be filled in, and in what order. Perhaps the right rule is to always use "show _, by apply_instance?" Is there documentation somewhere as to how resolution of superclass instances works and/or what we need to do to make it work?

view this post on Zulip Mario Carneiro (Apr 10 2021 at 04:39):

If the constructor actually takes a typeclass argument, you don't have to provide it like that. It's mainly when you use old structures that you need it since the C.mk doesn't actually have A and B as arguments but rather their fields

view this post on Zulip Kevin Sullivan (Apr 11 2021 at 02:01):

Mario Carneiro said:

If the constructor actually takes a typeclass argument, you don't have to provide it like that. It's mainly when you use old structures that you need it since the C.mk doesn't actually have A and B as arguments but rather their fields

Thank you.

view this post on Zulip Kevin Sullivan (Apr 12 2021 at 20:38):

Kevin Sullivan said:

Kevin Buzzard said:

I think you always have to put ..(show B, by apply_instance) in, even if the instance is in the type class cache.

Kevin B, thanks very much. The reason I ask is that Lean's behavior is inconsistent. Here's a piece of code that works without my saying anything about instances of superclasses (if I may use that terminology). I had mistakenly assumed that this is how Lean would work, in general. But clearly it's not.

class A (α : Type) := (n : nat)
class B (α : Type) := (m : nat)
class C (α : Type) extends A α, B α := (k : nat)

instance : A nat :=  1 
instance : B nat :=  2 
instance : C nat :=  3   -- works but maybe just by good luck

#reduce c                  -- {to_A := {n := 1}, to_B := {m := 2}, k := 3}

Ok, I see where my confusion was. First, my example above uses anonymous constructor notation, ⟨ ... ⟩. Typeclass inference appears to work to fill in the missing fields in the example I've given, but it doesn't appear to work in all cases. That's what had me misled: I'd drawn an inference from its working in simple cases to conclude that it works in general. I haven't yet quite figured out what's going on with that: when it works and when it doesn't. Second, it also appears that the ..p notation does not work at all with anonymous constructor notation. So, conclusion, it appears that combining standard { ... } structure instance definition notation with ..p, ..q, ..r notation (telling Lean to try to fill in missing field values from fields defined in p, q, r in that order) is what I need.

class A (α : Type) := (n : nat)
instance a : A nat :=  1      -- anonymous constructor notation

class B (α : Type) := (m : nat)
instance b : B nat :=  2      -- anonymous constructor notation

class C (α : Type) extends A α, B α := (c : nat)
instance c : C nat := { c := 3, ..a, ..b }  -- curly brace / field assignment notation

Last updated: May 10 2021 at 00:31 UTC