Zulip Chat Archive

Stream: new members

Topic: Little typeclass syntaxy thing


view this post on Zulip Mario Carneiro (Mar 07 2021 at 18:44):

You can't use dot notation on classes, because the typeclass argument of the projection (in this case ext_ext_has_op.op) is implicit

view this post on Zulip Mario Carneiro (Mar 07 2021 at 18:45):

you should write ext_ext_has_op.op α instead

view this post on Zulip Kevin Sullivan (Mar 08 2021 at 12:57):

Mario Carneiro said:

you should write ext_ext_has_op.op α instead

The language is a little funny in that it allows dot notation on classes, and it works sometimes but not others (when implicit instances need to be looked up). There are still two things I'm wondering about:

(1) Why exactly does binding m.op to mop then using mop work when using m.op directly doesn't?

(2) Where exactly should I write ext_ext_has_op.op α instead? Not seeing it.

view this post on Zulip Mario Carneiro (Mar 09 2021 at 04:58):

Yeah, that's a bug. It's not supposed to work at all

view this post on Zulip Mario Carneiro (Mar 09 2021 at 05:02):

def mul_foldr {α : Type u} [ext_ext_has_op α] [my_has_one α] : list α  α
| [] := my_has_one.one
| (h::t) := has_op.op h (mul_foldr t)

view this post on Zulip Mario Carneiro (Mar 09 2021 at 05:02):

@Kevin Sullivan

view this post on Zulip Mario Carneiro (Mar 09 2021 at 05:03):

Basically, you don't need to refer to variables in square brackets except in exceptional circumstances (which is why they are usually anonymous)

view this post on Zulip Kevin Sullivan (Mar 09 2021 at 19:02):

Mario Carneiro said:

Yeah, that's a bug. It's not supposed to work at all

That's helpful. Thanks for confirming. I knew that typeclass instances were generally anonymous, but had also seen a few instances where they weren't. It was also clear after a few minutes of thinking that there would be a problem finding implicit instances going up the stack lacking a sufficiently right context for inference. What wasn't clear was why the dot notation was supported at all. As a final question, if you've got a sec to complete this thread, can you characterize situations where it's necessary/helpful to have a non-anonymous (a "nonymous") typeclass instance?

view this post on Zulip Mario Carneiro (Mar 09 2021 at 19:42):

If you are using a lemma that takes a typeclass argument in () binders, you will need to specify it. This is sometimes done for typeclasses that are also props and intended to be used as such (i.e. participating in nontrivial logical positions like negations and disjunctions), like nat.prime. It's also necessary to specify typeclasses sometimes when the one that is inferred is not the one you want, which only happens occasionally, mostly when there is a non-defeq diamond in the typeclass hierarchy (which we try to avoid). Plus sometimes it's just the shortest way to write a proof

view this post on Zulip Mario Carneiro (Mar 09 2021 at 19:45):

Also it comes up when the typeclass itself has some structure on it and is the subject of the theorem, like this one from topology:

theorem ext [T : topological_space α] {σ : Type*} {F : ctop α σ}
  (H₁ :  a, is_open (F a))
  (H₂ :  a s, s  𝓝 a   b, a  F b  F b  s) :
  F.to_topsp = T :=
ext' $ λ a s, H₂ a s, λ b, h₁, h₂⟩, mem_nhds_sets_iff.2 _, h₂, H₁ _, h₁⟩⟩

view this post on Zulip Mario Carneiro (Mar 09 2021 at 19:46):

Here the type topological_space α is a typeclass, useful for providing topological structure on types, but it's also the space of topologies on α, which is a complete lattice with a map operator and interesting lemmas about it


Last updated: May 14 2021 at 00:42 UTC