Naming of new functions `tail∘inits` and `tail∘tails`

[MatthewDaggitt]

Just going through tidying up the CHANGELOG and came across PR https://github.com/agda/agda-stdlib/pull/2395 which introduced tail∘inits and tail∘tails.

This is the first time ever we've used unicode names for functions, and has potential to disrupt naming schemes in the Properties files.

Are we sure we want to do this? Could we come up with more conventional names for these functions? For example:

• tailInits/tailTails

[jamesmckinna]

Happy to take the suggestion (as I was for @andreasabel 's original suggestion of these names...)

I hadn't realised there was a prohibition on Unicode in function names (as opposed to those of properties).

Not thrilled by the new suggestions, but in a sense because these are 'only' helper functions, I'd be tempted to call them inits-aux and tails-aux instead? Or some variation on that?

Since @gallais pointed out in #2359 about using where clauses under a module declaration permits externally reference to locally where-defined, I had originally wondered about keeping the 'original' form of the definitions of inits and tails with these, their helper functions, defined locally, but then referring to them in this style... eg as Inits.aux and Tails.aux

Any (counter-) preferences out there?

[MatthewDaggitt]

Since @gallais pointed out in https://github.com/agda/agda-stdlib/issues/2359 about using where clauses under a module declaration permits externally reference to locally where-defined, I had originally wondered about keeping the 'original' form of the definitions of inits and tails with these, their helper functions, defined locally, but then referring to them in this style... eg as Inits.aux and Tails.aux

Thanks for the reminder! I would be strongly in favour of this as my new preferred solution.

[jamesmckinna]

Ah, just missed your latest comment... ... but having said that, I tried the 'localmodule' version... and the parameterisation/generalisation is wrong (or: not what my mental model thought it should be): defining

inits : List A → List (List A)
inits xs = [] ∷ tail xs
  module Inits where
    tail : List A → List (List A)
    tail []       = []
    tail (x ∷ xs) = [ x ] ∷ map (x ∷_) (tail xs)

Then Inits.tail is of type

{A.a : Level} {A = A₁ : Set A.a} → List A₁ →
{A.a = A.a₁ : Level} {A = A₂ : Set A.a₁} → List A₂ → List (List A₂)

Ie the parametrisation over xs is ... duplicated, because module Inits is defined in the scope of xs.

If you know how to fix this, I'll update #2413 to reflect that... or else feel free to yourself!

[JacquesCarette]

Pushing the xs to the rhs might do it?

[jamesmckinna]

Pushing the xs to the rhs might do it?

Indeed, see updated comment on #2413 ... can fix if you (collectively?) think it's better! And have, pre-emptively, done so.