typeclass names starting with `Is`?

Stream: mathlib4

[Kim Morrison]

Can anyone point me to a thread about the consensus on using Is in typeclass names for Mathlib? It isn't covered in #naming.

My understanding is that mixin Prop-valued typeclasses may/should start with Is, and Type-valued typeclasses must not. Is that accurate? How closely do we follow this in Mathlib? Is everyone happy? :-)

(There is some FRO internal discussion of naming that I'd like to provide context for.)

[Kevin Buzzard]

This is unfortunately not accurate -- docs#IsROrC is a counterexample (and I would certainly prefer that Is was used for Props only -- I remember Jeremy Avigad years ago telling me that this was stuck to in Isabelle and it made for easy understanding, so you might want to ask his opinion on the matter).

[Eric Wieser]

Conversely, docs#IsTensorProduct is a Prop, but I would prefer that it carried data

[Eric Wieser]

I guess we could rename IsROrC to ROrCLike, or more generally use Like as a suffix anywhere we are tempted to use Is for data?

[Adam Topaz]

Eric Wieser said:

Conversely, docs#IsTensorProduct is a Prop, but I would prefer that it carried data

Why?

[Anatole Dedecker]

Presumably to have the isomorphism with "the" tensor product bundled?

[Kevin Buzzard]

I would like a Prop-valued version of IsROrC which didn't choose a preferred $\sqrt{-1}$ (and which I'll write myself when I need it ) but probably this thread is not for these sorts of discussions.

[Adam Topaz]

Anatole Dedecker said:

Presumably to have the isomorphism with "the" tensor product bundled?

Is this actually useful though? In that case you may as well just use the tensor product itself.

[Jeremy Avigad]

I remember Jeremy Avigad years ago telling me that this was stuck to in Isabelle ...

I don't remember saying that or thinking that! Maybe that's a sign that I am now of a certain age. But the naming scheme does bring back memories of the old symbolic AI and object-oriented programming literature, e.g. this. Beyond nostalgia, I don't have any feelings about it.

[Adam Topaz]

Scott Morrison said:

My understanding is that mixin Prop-valued typeclasses may/should start with Is, and Type-valued typeclasses must not.

FWIW, I think such a naming convention makes perfect sense.

[Jireh Loreaux]

:up: this was my understanding, but I know we haven't been supercareful about it (like with IsROrC; maybe just ROrC?). I think it came from Lean 3 where we used is_foo : Prop and has_foo : Type* but then in Lean 4 core they dropped has, so Mathlib (mostly) did too. There are a few HasFoo relics now though.

[Eric Wieser]

Adam Topaz said:

Anatole Dedecker said:

Presumably to have the isomorphism with "the" tensor product bundled?

Is this actually useful though? In that case you may as well just use the tensor product itself.

It's useful constructively to avoid noncomputable. A reason you might not have the tensor product itself is to allow type aliases that put different norms / products on the tensor product, such as docs#GradedTensorProduct, which still "is" a tensor product

[Eric Wieser]

(react with :moving_truck: if you want me to split this discussion to a new thread)

[Jireh Loreaux]

Indeed, eventually I will be wanting to put norms on my tensor product.

[Eric Wieser]

Of course, this is maybe a failure in the use of type synonyms; any type that you might want to wrap in a synonym ends up needing an IsTheOriginalType typeclass.

[Winston Yin (尹維晨)]

My understanding is that mixin Prop-valued typeclasses may/should start with Is, and Type-valued typeclasses must not. Is that accurate? How closely do we follow this in Mathlib? Is everyone happy? :-)

docs#Embedding (Prop-valued mixin) and docs#Function.Embedding (bundled injective function) have been annoying me a bit. Technically doesn't violate what you're saying, which sounds like a decent rule, but IsEmbedding would be my preferred spelling for the former.

[Yaël Dillies]

Honestly, Embedding should live in the Topology namespace.

[Kevin Buzzard]

Some more counterexamples I noticed recently:

There are a whole bunch of TopologicalSpace mixins with no Is, e.g. CompactSpace, QuasiSober, QuasiSeparatedSpace, T0Space, T2Space,... .

Conversely there are a few category theory Is typeclasses which aren't Props; I found CategoryTheory.IsLeftAdjoint, CategoryTheory.IsRightAdjoint and CategoryTheory.IsEquivalence.

Note that #10819 changes the name of IsROrC.

[Anatole Dedecker]

Yes, in topology we have the conflicting naming convention of naming IsX properties about subsets and XSpace the corresponding property of spaces

[Kevin Buzzard]

When introducing new properties of topological spaces (what made me notice the list above was the discussion of spectral spaces here) should one always introduce the Is version for subsets too?

[Yury G. Kudryashov]

It depends on whether you want to deal with sets with this property.

[Yury G. Kudryashov]

Yaël Dillies said:

Honestly, Embedding should live in the Topology namespace.

We have things in Topology namespace and in TopologicalSpace namespace.

[Eric Wieser]

Anatole Dedecker said:

Yes, in topology we have the conflicting naming convention of naming IsX properties about subsets and XSpace the corresponding property of spaces

Can we move the former into the Set namespace?