Convention on composition order

Stream: general

[Sebastien Gouezel]

When one composes two functions f and g, the notation g ∘ f means: apply f first, and then g. However, since g is written first, one may want to replicate this in the definitions. For instance, the composition of linear maps takes g first and then f, and can be written as linear_map.comp g f, or as g.comp f. As far as I can tell, this is the convention that is mostly followed in mathlib. Let me call it (1).

However, there are examples in the other direction. For instance, the fact that the composition of two continuous functions g and f (I mean, g ∘ f) is continuous, is written as continuous.comp hf hg (where hf is the assumption that f is continuous, and similarly for hg). This can also be written as hf.comp hg. Let me call this (2).

I think this should be made coherent all over mathlib. I started to work on this, with the idea to convert everything to (1). However, it turns out that category theory follows convention (2), in

structure concrete_category (hom : out_param $ ∀ {α β}, c α → c β → (α → β) → Prop) :=
(hom_id : ∀ {α} (ia : c α), hom ia ia id)
(hom_comp : ∀ {α β γ} (ia : c α) (ib : c β) (ic : c γ) {f g}, hom ia ib f → hom ib ic g → hom ia ic (g ∘ f))

And I definitely don't want to mess with category theory without asking first here. Any opinion on this?

[Johan Commelin]

Big fights have been fought... epic stories can be told...

[Kevin Buzzard]

I find it really hard to care about this sort of question. I'm very happy indeed with the idea of being consistent. I don't care which convention we choose.

[Scott Morrison]

While I appreciate Kevin's commitment to not caring about silly issues like this, I want to argue that in certain flavours of higher category theory, writing things in "the right order " (i.e. (2)!) actually matters (because there might not even be a 'symmetry' allowing you to change the linear order of inputs!). I'm certainly not going to argue that this consideration says anything about the design of mathlib.

[Scott Morrison]

I recognise that I am sufficiently partisan/crackpot about this issue that I don't want my opinion taken too seriously in any of this. :-)

[Scott Morrison]

But my suggestion would be: in mathlib outside the category theory library, feel free to uniformise everything in the (1) convention, and in the category theory library, don't bother going to the enormous effort of moving away from (2). :-)

[Sebastien Gouezel]

I don't really care about the convention we choose. The basic problem is that the math notation is bad :) Let me go for (1) now just to see how it goes, while leaving category theory untouched as much as possible.

[Kevin Buzzard]

Philosophically speaking, I've always been ambivalent about this sort of thing because I have always been aware that in a parallel universe we could write maps on the right (i.e. write $(x)f$ for what mathematicians in this universe write as $f(x)$) and then composition conventions get turned on their head whilst the underlying ideas don't change. However in functional programming we write maps on the left and because this convention is baked in, perhaps this extends to some other conventions that we should adhere to.

[Johan Commelin]

I like how the unix shell got this right: cat foobar | grep something | tr 'abcde' 'ABCDE' | head

[Johan Commelin]

And don't get me started on "useless use of cat". There is no such thing as useless use of cat... :cat:

[Reid Barton]

I don't think I've seen (2) used in category theory except in an old paper of Barr which also write application in the other order ($XF$ for $FX$). Here is an Australian writing about enriched category theory using (1) in a place where it does make a difference.
Screenshot-from-2019-05-15-07-19-46.png
(Kelly, Basic concepts of enriched category theory, p. 8)

[Reid Barton]

(2) makes larger formulas hard to read when dealing with sets or presheaves of sets and their elements, or functors acting on objects, because of the reorderings in (f ≫ g) x = g (f x) and (F ⋙ G).obj x = G.obj (F.obj x)

[Scott Morrison]

Can we ask for function application to be written on the right in :four_leaf_clover:? :-)

[Keeley Hoek]

They already have camelCase
Stoke the fires of the revolution

[Sebastien Gouezel]

Done in #1035. I am sure I missed some instances, but I fixed notably continuous functions, measurable functions and derivatives. I only took care of comp stuff, which means that the order is not changed for trans stuff (in particular for equivs). Still looks much more coherent to me. Everything went smoothly (and tediously), except for some derivatives statements where Lean could not figure out the types I wanted when I changed the order, so I had to help it a little bit (see https://github.com/sgouezel/mathlib/blob/8cfe412cbb88d6a2d4f7a06f8a3f0600460b222c/src/analysis/normed_space/deriv.lean#L1139)

[Floris van Doorn]

Working on the category library a bit, it is confusing that (F ⋙ G).obj X is not definitionally equal to F.obj (G.obj X) but to G.obj (F.obj X). In other places, where you compose a bunch of morphisms or functors, it is more natural to think "from left to right", and have composition follow convention (2). So I agree with Kevin here in not really caring.

[Patrick Massot]

except for some derivatives statements where Lean could not figure out the types I wanted when I changed the order, so I had to help it a little bit (see https://github.com/sgouezel/mathlib/blob/8cfe412cbb88d6a2d4f7a06f8a3f0600460b222c/src/analysis/normed_space/deriv.lean#L1139)

That line is not pretty at all. Are you sure it does not reveal a deeper problem with the interface?

[Sebastien Gouezel]

That's a good question. I don't have a good answer here, as I don't know enough about how Lean tries to infer types (there are some heuristics at play, but here Lean gets it wrong).

[Reid Barton]

I'm a little more worried that, after monoidal categories, we'll get enriched categories with the opposite definition from the rest of the world.
Of course, from a math perspective it's just a matter of convention--like left modules vs right modules.

[Sebastien Gouezel]

Coherence with the rest of the world when it is possible looks like an important goal (to avoid increasing even more the entrance barrier). Unless the rest of the world is obviously wrong, of course.

[Sebastien Gouezel]

I would like to know if people are interested in #1035 (making sure that most comp lemmas use the same convention all over mathlib): as it touches many files, it will bitrot very quickly, and I don't know if my work in progress should be based on it or not. It would help me a lot if it could be either closed quickly, or merged quickly :)

[Johan Commelin]

I am in favour of merging this.

[Mario Carneiro]

I've approved it for merge

[Sebastien Gouezel]

Thanks!