containment _⊆_ generalization

[pnlph]

I saw that in Relation.Binary.Core is suggested (without expressing it formally) that the containment _⊆_ can be viewed as a synonym of the implication _⇒_

agda-stdlib/src/Relation/Binary/Core.agda

Lines 43 to 46 in 99367e2

	-- Implication/containment - could also be written _⊆_.
	_⇒_ : REL A B ℓ₁ → REL A B ℓ₂ → Set _
	P ⇒ Q = ∀ {x y} → P x y → Q x y

Then in Data.List.Relation.Binary.Sublist.Setoid the symbol of containment _⊆_ is used to express containment restricted to Lists.

agda-stdlib/src/Data/List/Relation/Binary/Sublist/Setoid.agda

Lines 40 to 41 in 99367e2

	_⊆_ : Rel (List A) (c ⊔ ℓ)
	_⊆_ = Heterogeneous.Sublist _≈_

Should not _⊆_ be reserved to express general containment and then notate the specific containments in another way, eg, _⊆ₗᵢₛₜ_?

[gallais]

If you need to use both notions simultaneously, you can always import
Data.List.Relation.Binary.Sublist.Setoid qualified as List and write
xs List.⊆ ys.

I'd rather have the short name that can be used when things are not ambiguous.

[MatthewDaggitt]

Addressing the second point first:

Should not ⊆ be reserved to express general containment and then notate the specific containments in another way, eg, ⊆ₗᵢₛₜ?

My question would be why is the subset relation over binary relations the correct notion of "general containment"? We also have subset relations over unary relations (predicates) and indeed in certain contexts you can even view a function from A to B as saying that A is a subset of B. Having unique names for all of these concepts would involve a lot of overhead. In many situations users have only imported a single instance in which case the disambiguation only serves to add noise.

Basically we seek to optimise the common case, and in the uncommon case then you can either qualify the module, or manually rename it to your desired disambiguation.

As implication vs containment, I don't really have an opinion. That's simply the way the library was set up many years ago. It's a pretty crucial component of the library so we'd need a strong reason for renaming it.

[pnlph]

Thank you, your answers were very informative.

I'd rather have the short name that can be used when things are not ambiguous.

Basically we seek to optimise the common case, and in the uncommon case then you can either qualify the module, or manually rename it to your desired disambiguation.

I think it would be good to expand with this kind of information the style-guide, a how-to guide or similar so that demands like the one in this reddit post could be covered:
Agda coding style guide? Naming suggestions?

There won't be any silver bullet: naming is hard and unless something is an (instance of an) established notion in mathematics or programming, you'll have to come up with one yourself. Having refactoring tools to easily rename definitions would definitely be a plus though.

Is it possible to assist the user in building her own set of naming conventions, or this falls out of the scope of the library? Until now, I just found the naming conventions section of the style guide.

[MatthewDaggitt]

Is it possible to assist the user in building her own set of naming conventions, or this falls out of the scope of the library? Until now, I just found the naming conventions section of the style guide.

I think adding it to the style guide is a good idea. I've added it to my list of things to add, which will get flushed before the release of 1.3