Fixities of `_<$>_` functions

[Sofia-Insa]

Should all the functions _$_ , _⟨$⟩_,_<$>_, _<$_ ... have the same fixity ?

README.Design.Fixity : -- application infixr -1 _$_ _$!_

• infixr -1 & infix -1

  • infixr -1 _$_ | Function.Base
  • infixr -1 _$!_ _$!′_ | Function.Strict
  • infixr -1 _<$>_ _<*>_ | Data.Container.FreeMonad
  • infix -1 _$ⁿ_ | Data.Vec.N-ary

• infixl 1

  • infixl 1 _<$>_ | Function.Nary.NonDependent.Base
  • infixl 1 _<$>_ | IO.Base

• infixl 4

  • infixl 4 _<$>_ _<$_ | Effect.Functor.Predicate
  • infixl 4 _<$>_ _<$_ | Effect.Functor
  • infixl 4 _<$>_ _<*>_ _<$_ | Reflection.TCM.Syntax

• infixl 5

  • infixl 5 _⟨$⟩_ | Function.Equality
  • infixl 5 _⟨$⟩ʳ_ _⟨$⟩ˡ | Data.Fin.Permutation

• infixl 6

  • infixr 6 _$ʳ_ | Tactic.RingSolver

• No fixity

  • _<$_ | IO.Base

[jamesmckinna]

Interesting and varied collection!

The stand-out label:low-hanging-fruit is the last entry, but I'm not clear if it should simply have the same fixity as _<$>_... but that seems a reasonable starting point.

As to the others, it seems as though the fixities have been chosen precisely to be distinct from function-application instances of the same idea, so the question (to me, not a fixity expert! I find it ends up being a matter of guesswork, or else emulation of existing exemplars, more than cold calculation of how I might want complex expressions to achieve unambiguous parses...) would be whether they should all be set at 4,5 or 6.

One way to do this might be to go back to the original authors and poll them on their choices?

[JacquesCarette]

The question arose because of trying to give all operators fixities. "What fixity" is what led us down this road of finding what looks like a lot of inconsistencies. I agree that it should the same fixity as _<$>_ ... but which one?!

There seems to be some unrecorded design knowledge embedded in these choices that we ought to recover and record. I guess the next step is to use git blame to figure out the original authors (@Sofia-Insa please do this) and for me to ask them if they can recall their design.

[gallais]

My assumption is that the fixity of the applicative connectives is lifted from Haskell.

[Sofia-Insa]

• infixr -1 _$_ _$′_ _$!_ _$!′_ | Function.Base & Function.Strict

  • infixr 0 → infixr -1 in 497e4dd to fix Issue Breaking change: give _$_ a fixity of -1 #351

• infixr -1 _<$>_ _<*>_ | Data.Container.FreeMonad

  • Fixity added in eb27a74 (PR Fixities for Data and Codata #1989 )

• infix -1 _$ⁿ_ | Data.Vec.N-ary

  • Fixity added in df8bdd4 (PR Fixities for Data and Codata #1989 )

• infixl 1 _<$>_ | IO.Base

  • _<$>_ and its fixity added in 87b26d9 ( PR [ refactor ] Clean up the dependency graph #1435)

• infixl 1 _<$>_ | Function.Nary.NonDependent.Base

  • Fixity added in 1309c75 (PR Fixity #1228)

• infixl 4 _<$>_ _<$_ | Effect.Functor.Predicate

  • Fixity added when the file was created 0801d08

• infixl 4 _<$>_ _<$_ | Effect.Functor

  • Fixity added when the file was created 596e140 it was then called Category.Functor

• infixl 4 _<$>_ _<$_ | Reflection.TCM.Syntax

  • Fixity was added when the file and the functions were created f452497, the file was then called Reflection.TCMonadSyntax

• infixl 5 _⟨$⟩_ | Function.Equality

  • Fixity added when the function was renamed in 20b3641, then, the file was named Relation.Binary.FunctionSetoid

• infixl 5 _⟨$⟩ʳ_ _⟨$⟩ˡ | Data.Fin.Permutation

  • PR Adding Data.Fin.Permutation #252 _⟨$⟩ʳ_,_⟨$⟩ˡ_ added to the file without fixity by alexarice@6dfa51c
  • PR Add transposition decomposition for permutations #1271 infixl 5 added in c0b326b

• infixr 6 _$ʳ_ | Tactic.RingSolver

  • fixity added 1309c75 PR Fixity #1228

[JacquesCarette]

I've asked around why Haskell's fixities are the way they are - we'll see if I get an answer. It certainly feels like the various <$> operators should have the same fixity as each other (no a mixture of 4-5-6).