Rename record fields for functorial actions and components of natural transformations

[sstucki]

TL;DR

I really, really, don't like the names of the fields F₀, F₁ and η in the Functor and NaturalTransformation records.

Below, I explain why and suggest some alternatives. However, I realize that changing these names would affect just about every file in the library and completely break compatibility with older versions. So I think any such change should be thoroughly discussed first. That is the purpose of this issue.

Why I don't like the current names

In my opinion it's not a good idea to conflate the name of a projection (field name) with the typical name of an instance of the record it belongs to. There two reasons for this:

1. Functors are typically called F, and their functorial actions F₀ and F₁, so as long as there's only ever one functor, it makes sense to use this convention for the fields of Functor. Then we simply open Functor F and everything looks just like it is supposed to.

   But only until there are two or more functors. Then one gets unreadable code of the form F₀ G which just doesn't make sense, IMO. The same goes for the components of natural transformations. As long as there is only one, η is fine. But with two or more, we get letter soup like this excerpt from Category.Construction.Functors:

     let open NaturalTransformation
         open Functor
     in begin
       (η β C ∘ η α C) ∘ F₁ F (g C.∘ f)  ≈⟨ refl ⟩∘⟨ homomorphism F ⟩
       (η β C ∘ η α C) ∘ F₁ F g ∘ F₁ F f ≈⟨ assoc ⟩
       η β C ∘ η α C ∘ F₁ F g ∘ F₁ F f   ≈⟨ refl ⟩∘⟨ pullˡ (commute α g) ⟩
       η β C ∘ (F₁ G g ∘ η α B) ∘ F₁ F f ≈⟨ refl ⟩∘⟨ assoc ⟩
       η β C ∘ F₁ G g ∘ η α B ∘ F₁ F f   ≈˘⟨ assoc ⟩
       (η β C ∘ F₁ G g) ∘ η α B ∘ F₁ F f ∎
   

   One can of course get around this by renaming things locally (e.g. open Functor G renaming (F₀ to G₀; F₁ to G₁), and so on) but that just seems a like a hack to me (and it introduces lots of noise in the code).

2. Another reason I don't like it is that F is so short and generic. I'd like to have F₀ available as a variable name. For example, if there are 3 or more functors, I might want to call them F₀, F₁ and F₂, but the projection pollutes the namespace. This is even worse for η since there are lots of things called η. For example, the units of adjunctions or monads, or the η-laws of lambda calculi (and CCCs).

(See this comment for the initial discussion that started this issue.)

Possible alternatives

When implementing the enriched versions of Functor and NaturalTransformation, I played arround with some alternative options. After a discussion with @JacquesCarette, we settled on map₀ and map₁ for the functorial actions for now. These are a good deal longer than F₀ and F₁, so the Functor record contains two alias definitions ₀ = map₀ and ₁ = map₁ that can be used to mimic the usual notation. See the functor module code for example usage.

I'm quite happy with that choice, but of course, there are many other possible names. E.g. for map₀ I considered the alternatives act₀, action₀, omap, obj-map, _$₀_, etc.

For enriched natural transformations, the current version of the record uses comp (for component) instead of η, and an alias _[_] to lighten notation (see the current implementation here, and another example usage here).

I'm less happy about that choice. @JacquesCarette conducted a little survey of naming conventions used by other libraries and found the following:

• η
• α
• components_of
• nt_component
• ApNT
• transform (with notation transform[_] for extraction)
• natural_map (with a coercion added so that the name of the NT can be used as a function, which is nice but leads to coercion hell)
• indmor
• NatTransMap (with notation $$ for application)

Human-readable vs. symbolic names

Personally, I have a slight preference for human-readable names over symbolic ones (one can always introduce symbolic aliases later) but I don't mind notation being symbolic if that turns out to be more convenient.

There is no reason one cannot have both, though. One can always introduce symbolic names through a custom "record module" like so:

module FunctorShort = Functor hiding (₀; ₁) renaming (map₀ to _₀; map₁ to _₁)

Then one can write this style of code:

open Category
open FunctorShort  -- open the alternative "record module"

_∘F_ : Functor D E → Functor C D → Functor C E
_∘F_ {C = C} {D = D} {E = E} G F = record
  { map₀     = λ X → (G ₀) ((F ₀) X)
  ; map₁     = G ₁ ∘ F ₁
  ; identity = begin
      (G ₁ ∘ F ₁) ∘ id C   ≈⟨ pullʳ (identity F) ⟩
      G ₁ ∘ id D           ≈⟨ identity G ⟩
      id E                 ∎
  -- ...
  }

[HuStmpHrrr]

a related issue is the naming convention #5

[HuStmpHrrr]

another sort of bad naming which has been address #2

[sstucki]

Thanks for the pointers @HuStmpHrrr! Indeed, #2 is exactly the same sort of bad naming IMO. I'm glad this got changed. Another example are some of the fields in Product.

Unrelated: could the description in #5 be copy-paste into a contributors guide? Of course that would be just a start (there's more that should be said in such a guide), but it's better than nothing's! I was looking for something like that but it's a bit hidden in the issues IMO.

[HuStmpHrrr]

I guess it is actually very good to bring up this issue as early as now. having external dependencies is not a problem, if we only break them hard once; changing the names bit by bit will break them hard again and again, and that's the truly terrible thing.

admittedly, there are terrible names in this library. most of them are inherited from the previous library. so if we are to review them, we should do it now. I guess I will start with my preference.

My Preference

I never like open X renaming (foo to bar). in particular, renaming is very difficult to track without running in Emacs (and sometimes even running in Emacs). it's hardly intuitive because what renames to what is somewhat an adhoc decision, and thus less fruitful. what's worse, renaming usually happens in a where block, which confuses me half way through, until I hit the right place after scrolling 100 lines. for that reason, I usually only rename infix operators. I especially dislike this kind of renaming:

  open Functor G renaming (F₀ to G₀; F₁ to G₁)

or even

  open Functor F
  open Functor G renaming (identity to G-identity)

in the previous library, this kind of renaming is everywhere, and I can't read anything. that brings up my preference, operating by record modules.

record in Agda is wonderful in that it also constructs a module. for example, module G = Functor G, allows us to access G.F₀ and G.identity, etc. arguably, G.F₀ is better than renaming to G₀, and G.identity is certainly the clearest. that said, I think the post-fix operators _₀ and _₁ is the best for Functors. it's clean and intuitive, so I think we should have it, but otherwise, taking advantage of record modules are simply the best practice. provided that we know what the arguments are, which is mandatory to understand the functions anyways, dot accessors keep everything very stylistic consistent.

with record modules, then, i see no big reason to open record modules wildly, like open Functor or open NaturalTransformation. we sometimes need it because we have some ad-hoc Functor construction, for example, but it won't happen too often. If we need to construct an auxiliary Functor and refer to it frequently, then why not give it a (private) name and a module so we can dot accessing everything as deep as possible? I've been very careful about defining modules of records inside of records so dot accessing can go really deep, which can only improve readability. For example, record modules will turn the example above into

β.η C ∘ α.η C

it appears immediate to me what's happening.

Field Names

I do think mappings and components of Functor and NaturalTransformation are not the best. The names are too short and too general, so we should probably change them, but they shouldn't be too long either. I think it's less a problem in other systems like Coq, which, for example, has coercion which can coerce a natural transformation to a function in a function context, so it doesn't really hurt to have a longer name. In Agda, longer field names will appear everywhere so it won't be too nice. I think for Functor, map₀ and map₁ are decent, provided the post-fix operators _₀ and _₁.

for NaturalTransformation, I agree a single Greek letter is too short.comp looks ok. we want to be careful about what the infix operator for component looks like. _[_] is used for natural transformation between enriched categories but I would argue it's not the best. [_] is really everywhere: it's a singleton list, it's the constructor for inspect pattern and it also shows up in Commutation syntax. I'd suggest to use a pair of different brackets. we can pick some from here: https://people.inf.elte.hu/divip/AgdaTutorial/Symbols.html#parentheses

we should also look at other records. if we are to change NaturalTransformation, then Dinatural should also be a candidate. it uses α which is the worst (my bad). however, in some other concepts, it does not appear as bad. for example, for a Monad, the natural transformations seem a bit more reasonable to keep it as is, due to https://ncatlab.org/nlab/show/monad, though it might also be a good idea to make the functor T, which appears to me more conventional.

It would be nice if we go through all the concepts in general one by one and see if any field names are unreasonable, and fix them along the way.

I also want to make a concrete suggestion on how the names should be fixed. I think the best way to fix it is one definition at a time. that is, we fix Functor everywhere, then this fix is one commit, then NaturalTransformation, etc. each concept corresponds to a fix in one commit, so if revert needs to happen, it can happen quick.

[HuStmpHrrr]

there are almost too many broken design decisions inherited from the previous library. if anything, we should address them as early as possible.

[sstucki]

Thanks for your comments @HuStmpHrrr!

I agree with most of what you say.

Here are detailed responses to some of your comments:

in particular, renaming is very difficult to track without running in Emacs (and sometimes even running in Emacs). it's hardly intuitive because what renames to what is somewhat an adhoc decision, (...)

Indeed. Maybe we should have guidelines/conventions for what are acceptable/expected cases for renaming.

what's worse, renaming usually happens in a where block, which confuses me half way through, until I hit the right place after scrolling 100 lines.

Indeed. This could be avoided by opening modules and defining shorthands up-front if necessary. Maybe that would be another good convention to add to a contributors guide.

record in Agda is wonderful in that it also constructs a module. for example, module G = Functor G, allows us to access G.F₀ and G.identity, etc. arguably, G.F₀ is better than renaming to G₀, and G.identity is certainly the clearest.

I like post-projections on modules too. I wish post-projections on terms (rather than modules) worked in the same way though. Then we could omit the clutter of all these module X = Record X definitions. But alas, that's not the case. There's an option to enable post-projections on record terms (using {-# OPTIONS --postfix-projections #-}) but they don't look as nice as the projections on modules. (See example below.)

that said, I think the post-fix operators _₀ and _₁ is the best for Functors.

I'm not convinced. Here are four options for functors that I think are acceptable. All with advantages and drawbacks:

1. Module post-projections ₀ and ₁

   let module F = Functor F
       module G = Functor G
   in F.₀ (G.₀ X)
   

   • Pros: looks great, very intuitive
   • Cons: lots of module definitions required, which clutter the code

2. Term post-projections ₀ and ₁

   F .₀ (G .₀ X)   -- requires {-# OPTIONS --postfix-projections #-}
   

   • Pros: no module definitions needed
   • Cons: the extra space is distracting/hard to parse; postfix projections are an experimental Agda feature

3. Postfix operators _₀ and _₁

   (F ₀) ((G ₀) X)
   

   • Pros: very concise, close to mathematical notation
   • Cons: lots of extra parentheses required, reduces readability

4. Infix operators _$₀_ and _$₁_ (right-associative)

   G₁ $₀ H₁ $₀ X
   

   • Pros: low overhead, readable, _$_ operator is "known" to Haskell/Agda programmers
   • Cons: the $ looks weird/disruptive to non-experts

(...) taking advantage of record modules are simply the best practice. provided that we know what the arguments are, which is mandatory to understand the functions anyways, dot accessors keep everything very stylistic consistent.

I agree this is the cleanest choice from a readability and consistency point of view.

(...) For example, record modules will turn the example above into

β.η C ∘ α.η C

it appears immediate to me what's happening.

Indeed. Except, I still don't like mixing α and η in this way. There must be a better notation.

I think for Functor, map₀ and map₁ are decent, provided the post-fix operators _₀ and _₁.

Agreed. I think having both human-readable names and symbolic ones makes sense (irrespective of exactly which shorthand/symbolic names we decide to pick in the end).

_[_] is used for natural transformation between enriched categories but I would argue it's not the best. [_] is really everywhere: it's a singleton list, it's the constructor for inspect pattern and it also shows up in Commutation syntax. I'd suggest to use a pair of different brackets. we can pick some from here: https://people.inf.elte.hu/divip/AgdaTutorial/Symbols.html#parentheses

I agree that square brackets are hopelessly overloaded. I'm fine picking some other type of parentheses, provided they remain readable (and reasonably easy to type).

we should also look at other records. if we are to change NaturalTransformation, then Dinatural should also be a candidate.

Completely agree. Once we pick a notation, it should be enforced consistently. (Same with functors and pseudofunctors, etc.)

however, in some other concepts, it does not appear as bad. for example, for a Monad, the natural transformations seem a bit more reasonable to keep it as is, due to https://ncatlab.org/nlab/show/monad, though it might also be a good idea to make the functor T, which appears to me more conventional.

I agree. When there is an existing convention, we should try to follow it. Also, in the case of components (e.g. the unit of a monad) where there's no confusion with the concept they belong to (e.g. the monad) there's no problem of naming them in the usual way. In the monad case, the problem arises if we call both the monad instance and its functor component T. In that case, the latter should probably be called functor or something of that sort.

I also want to make a concrete suggestion on how the names should be fixed. I think the best way to fix it is one definition at a time. that is, we fix Functor everywhere, then this fix is one commit, then NaturalTransformation, etc. each concept corresponds to a fix in one commit, so if revert needs to happen, it can happen quick.

Agreed. I'd go so far as introducing a separate issue for each of these, refactor everything in a separate branch (per issue), test it, create a PR from the branch and review it to double check everything looks OK.

[HuStmpHrrr]

I am not a fan of any extra options, if they are not already stable. I didn't know that option. probably we can ask to improve it. for

(F ₀) ((G ₀) X)

I believe we can drop two pairs of parens, can't we?

F ₀ (G ₀ X)

the only pair left does not seem avoidable.

in the monad case, if we are talking about more than one, we can do module M = Monad M; module N = Monad N, etc. then M.T and N.T distinguish both and it's very clear which is which. but opening Monad and then T M and T N is bad because the current name space is polluted by a very short name.

I guess the question lies to how we can reduce too many module X = Foo X kind of code. IMO, it's not an urgent problem at the very least, because such code is close to line noise as long as we keep the names consistent.

[sstucki]

(F ₀) ((G ₀) X)

I believe we can drop two pairs of parens, can't we?

F ₀ (G ₀ X)

I tried that and it didn't work. I suspect it's to do with precedence: function application has higher precedence than infix operators. But maybe there's a way around that that I don't know about.

A slightly hacky solution is to add an extra underscore to the operator: _₀_ instead of _₀. Then one doesn't need the extra parentheses, but the whole expression still has lower precedence than any application it might be part of, and partial applications look ugly (same as for _$₀_).

Feel free to experiment and let us know if you find a version that works.

[HuStmpHrrr]

then F.₀ is just clean. a dot in the middle is not too disturbing.

[JacquesCarette]

I waited a while on this one, as I wanted to really think about it. I definitely agree it's an issue, and that we ought to deal with it [if at all] sooner rather than later.

I agree with the basic problem. When there is a single Functor around, the 'puns' allowed by the current naming is cute - but it doesn't scale. And so on for the other cases.

I am not personally all that against renamings. Although I agree that renamings in where clauses are a problem, since you need to go "all the way down" to first figure out what the names in scope are, then back up to understand the details. I've been experimenting with putting these in let clauses at the top instead. But I'm biased here, as I use renamings as a feature in other contexts. I'm quite happy with a solution that doesn't involve renamings as they are not first-class enough in Agda.

It seems to me that named modules currently offer the best compromise. Also, I think we might be able to lobby for having these be available even more easily [i.e. some simpler syntax to do the obvious thing].

---

For the case at hand, I agree that for Functor, those two module post-projections are nice.

For NT, I wonder if the lower parens (i.e. \_( and \_) in emacs mode) would be better than [_]? They are fairly easy to type, and have a 'lower' connotation which could invoke the subscript notation usually used.

[sstucki]

I am not personally all that against renamings. Although I agree that renamings in where clauses are a problem, since you need to go "all the way down" to first figure out what the names in scope are, then back up to understand the details. I've been experimenting with putting these in let clauses at the top instead.

I agree. Sometimes renamings lead to much more readable code, and in such cases I'm all in favor. (I used this approach recently in #110 and #111.) I also completely agree that it's bad to introduce such renamings in where clauses. In addition to let open clauses, there's also the option to open a module (or define a shorthand) that is used throughout a module at the beginning of the module (with private modifiers where necessary).

It seems to me that named modules currently offer the best compromise. Also, I think we might be able to lobby for having these be available even more easily [i.e. some simpler syntax to do the obvious thing].

That would be great. Not sure what this would look like though. Do you have concrete suggestions?

For NT, I wonder if the lower parens (i.e. \_( and \_) in emacs mode) would be better than [_]? They are fairly easy to type, and have a 'lower' connotation which could invoke the subscript notation usually used.

I like that suggestion very much! 👍 I'll try it out in the "enriched" modules and submit a PR if it looks nice.

[JacquesCarette]

I don't yet have a concrete suggestion on how to make it easy to have named modules for the corresponding record in Agda - but I have started thinking about it.