[ deprecate ] one of `Function.Core` *or* `Algebra.Core`

[jamesmckinna]

It's not obvious to me that we ever make use of this module.

Moreover, its functionality is largely duplicated by Algebra.Core, while Morphism as a definition seems deprecated/unused everywhere else, except as a public re-export in Relation.Binary.Morphism.Definitions cf. #2875 / #2922 UPDATED: ah... but see #1206 / #1213

The alternative would be to deprecate (?), or else simply leave as a stub, Algebra.Core, as:

module Algebra.Core where

------------------------------------------------------------------------
-- Unary and binary operations

open Function.Core public
  using ()
  renaming (Fun₁ to Op₁; Fun₂ to Op₂)

[MatthewDaggitt]

We have found Algebra.Core and Relation.Binary.Core very useful in breaking dependency cycles. I therefore added Function.Core under the assumption that it would be similarly useful. If we want to remove it, I guess we should at least try to understand why the former two are useful but the latter is not?

[jamesmckinna]

So my understanding (thanks for the context/history update) would be: we only really have Function.Core for Morphism, as requested (for pedagogical purposes) by @pnlph . So in that sense, it remain 'useful' (whereas Fun₁ and Fun₂ seem... moot? They're really never used anywhere, except for their redundant recapitulation in Algebra.Core).

I can believe that, at least in principle, having a Z.Core module at the root of hierarchy is a convenient placeholder for extremely common definitions which would otherwise create dependency cycles/DRY violations. And there very well may be more to come in the future...

But the DRY violation in Algebra.Core (Op₁ and Op₂ in place of/duplicating Fun₁ and Fun₂) is perhaps the one stand-out (and why I modified the title of the issue, as my knowledge of/instinct towards the issue shifted), and I guess is also (a)historical, but now, could be refactored away, as indicated, if we opt to retain Function.Core.

Arguably, this is pure bikeshedding, but downstream/eventually/maybe never, the current setup seems a wart which we could 'tidy up'.

But happy to file this under hypothetical-rewrite... it surely can't be a deal-breaker ;-)

[JacquesCarette]

I actually find that Fun₁ (and Op₁) for all arities tends to make code more obscure. So while it is "too late" for Algebra (i.e. that ship has sailed, and reconsidering that shouldn't even be on the table for v3.0, but only for hypothetical-rewrite), since it isn't really used, I'm all for deprecating Function.Core.

[jamesmckinna]

Thanks @JacquesCarette . I hadn't thought that anyone would want to go as far as deprecating Algebra.Core but, indeed, perhaps one day.

For now though, not that anything need be done now (or ever, given your hypothetical-rewrite aside), and after the more historically informed insights from you and @MatthewDaggitt I'd be tempted to close this issue with the status quo untouched.

I'm conscious of (perhaps) too many issues lying open for years, and let's not add this one to that pile.