RFC: names for different bundlings of the same function

Stream: mathlib4

[Anatole Dedecker]

I'm getting somehow annoyed by the different conventions we have for naming the same map but bundled in different ways. For example, compare the naming of docs#ContinuousLinearMap.compContinuousMultilinearMapL, docs#ContinuousMap.evalClm, docs#SchwartzMap.evalCLM, and so on... Unless someone has a magic way to allow the use of morphism classes here (I may actually have one which is a bit ugly, see below), I would like to decide on a general naming scheme here.

One thing that would be realy nice imo is being able to tell at a glance which part of the name refers to the name of the map, and which part refers to the bundling. Natural options would be to use nameOfMap.type or nameOfMap.asType, e.g ContinuousMap.evalClm could become ContinuousMap.eval.asContinuousLinearMap. I think it makes sense to also allow abbreviations here as long as they are clearly documented (e.g Clm for ContinuousLinearMap, or Bcf for BoundedContinuousFunctions), and they are also a thousand variations we could choose from (maybe we just write .continuousLinear?). The thing I really like with having the dot as a separation is that it's clearer semantically, especially in cases where the name has to contain two hom names like docs#ContinuousLinearMap.compContinuousMultilinearMapL.

I'd like to get opinions on that (and other naming suggestions in the same vein!), because I feel like this is getting out of hand quite quickly...

[Eric Wieser]

Note that things are sometimes doubly bundled, like docs#LinearMap.llcomp

[Anatole Dedecker]

I think this one could reasonably be called docs#LinearMap.comp.asBilinear but I agree that it's not ideal. Of course there are a bunch of edge cases like these that we need to think about!

[Eric Wieser]

Another option would be to have LinearMap.eval be fully unbundled, and then have the spelling be LinearMap.of (LinearMap.eval)

[Eric Wieser]

(via the return of an IsLinearMap typeclass)

[Anatole Dedecker]

Re: potential way to make use of morphism classes.

We could make each morphism that needs to be highly bundled have its own type (typically a singleton of itself), make this type FunLike and add bunch of HomClass instances to it depending on some assumptions. The problem is that gets annoying as soon as the map depends on some data, because introducing dependent types when we don't need them is not a good idea...

[Anatole Dedecker]

Of course the other solution is IsLinearMap, but that sounds like opening a can of worms...