Zulip Chat Archive

Stream: new members

Topic: How to access typeclass values?


view this post on Zulip Nicholas Dyson (Dec 04 2020 at 14:47):

I'm just learning how to use typeclasses in Lean, and the documentation seems sparse. Specifically, how do I refer to elements from the typeclass definition when proving results about all types that are a member of a typeclass?

As a simple example, suppose I have the default "inhabited" class:

class inhabited (α : Type _) :=
(default : α)

And suppose I want to define and prove the utterly trivial result that for any type that is a member of the "inhabited" class, the default element is equal to itself. I have no idea what the syntax for this would be. In an informal syntax (because if I knew how to express these concepts in Lean syntax, I wouldn't be asking this question), what I'm aiming for is expressing something like:

( t : Type) [(inhabited t) -> (t.default = t.default)]

if that makes sense. So what I need is to

  • declare a lemma over an arbitrary type t so long as that type is a member of a given typeclass, and then
  • access the values of type t that the typeclass definition tells us exist.

Hope that makes sense, I'm finding this a challenging concept to explain. Thank you very much for any advice.

view this post on Zulip Mario Carneiro (Dec 04 2020 at 14:52):

You want ∀ (t : Type) [inhabited t], inhabited.default t = inhabited.default t

view this post on Zulip Mario Carneiro (Dec 04 2020 at 14:54):

except that won't work directly because of typeclass caching, so you have to insert a by exactI to make typeclass inference work:

 (t : Type) [inhabited t], by exactI inhabited.default t = inhabited.default t

view this post on Zulip Mario Carneiro (Dec 04 2020 at 14:57):

class inhabited' (α : Type _) :=
(default [] : α)

example (α) [inhabited' α] : inhabited'.default α = inhabited'.default α := rfl

view this post on Zulip Mario Carneiro (Dec 04 2020 at 14:58):

I had to put [] in in order to make the alpha explicit in default; the alternative would be

class inhabited' (α : Type _) :=
(default : α)

example (α) [inhabited' α] : (inhabited'.default : α) = inhabited'.default := rfl

view this post on Zulip Nicholas Dyson (Dec 04 2020 at 16:45):

Thank you this was very helpful.


Last updated: May 14 2021 at 04:22 UTC