Little typeclass syntaxy thing

Stream: new members

[Mario Carneiro]

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

[Mario Carneiro]

you should write ext_ext_has_op.op α instead

[Kevin Sullivan]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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)

[Mario Carneiro]

@Kevin Sullivan

[Mario Carneiro]

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

[Kevin Sullivan]

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?

[Mario Carneiro]

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

[Mario Carneiro]

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₁⟩⟩

[Mario Carneiro]

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