Can we unify Relation.Binary.Morphism.Definitions and Function.Definitions?

[Taneb]

Relation.Binary.Morphism.Definitions has as module parameters the domain and codomain of the functions over which the definitions are made, whereas Function.Definitions has them in a variable block. The former module only contains Homomorphic₂, which is exactly the same as the latter's Congruent, and a re-export of Morphism from Function.Core, which I think is otherwise unused in the library (and is just a synonym for the function arrow).

Can we deprecate Relation.Morphism.Definitions in favour of Function.Definitions?

[jamesmckinna]

"Can"? or "Should"?

It seems as though (modulo dependencies/dependency cycles? not sure about this...) we can.

Not obvious to me that we should... partly because of the ergonomics of the whole Algebra hierarchy... that eventually rests on Relation.Binary (and IsRelHomomorphism specifically), and swapping out a Relation.Binary component in favour of a Function one, even if semantically equivalent/justified, seems like a rupture (however small) in the design hierarchy? Maybe this is a nonsense argument, but the "what are all the things I need to import to get task X done?" question (allied with the lack of suitable search tools) means that I like not having to look 'outside the box' for functionality if I can avoid it... but this is off the top of my head, without a serious analysis of the situation.

[MatthewDaggitt]

I agree with @jamesmckinna. We absolutely can, but I don't think we should because it would be violating the standard design of hierarchies in the library. Obviously if we could do it for every hierarchy in the library that would be a different question....

[jamesmckinna]

Revisiting this in the course of reconsidering #1436 ... not to go back on my earlier judgment, but to observe that if Function.Definitions were instead to take the two (implied) RawSetoid arguments as top-level module parameters (rather than local to the internal anonymous module), then we could at least achieve some reconciliation with Algebra.Definitions wrt Congruent/Monotonic and Injective/Cancellative, with a little gymnastics. But is that worth the trouble?

Eg. inFunction.Structures, we would instead have:

module Function.Structures {a b ℓ₁ ℓ₂}
  {A : Set a} (_≈₁_ : Rel A ℓ₁) -- Equality over the domain
  {B : Set b} (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain
  where

open import Data.Product.Base as Product using (∃; _×_; _,_)
open import Function.Base
open import Function.Definitions _≈₁_ _≈₂_
open import Level using (_⊔_)

in the preamble, and thus not endlessly have to repeat the explicit parameters _≈₁_, _≈₂_ to Congruent etc. throughout.

(And yes, the module is instantiated at different relations at various points, so better would be to have a qualified import, and then supply the parameters... but this doesn't really vitiate the point)

Ditto. in the concrete Data modules, where _≈₁_, _≈₂_ are given by PropositionalEquality, again the use of Injective etc. could be streamlined by opening the module with those parameters supplied.

Ditto. in Relation.Binary.Morphism.Structures and hence in Algebra.Morphism.Structures, which I guess was @Taneb 's original motivation? The subtle variation in parametrisation between all these modules is striking once you stare at them for long enough...

(Unless I really don't understand how module instantiation works... I'm guessing that

module Foo (p : P) where
  defn : ...
  defn = ...

is not the same, on import, as

module Foo where
  module _ (p : P) where
    defn : ...
    defn = ...

or are these two 'the same'?)

[jamesmckinna]

... And the above remarks apply also to Algebra.Consequences, where it would (perhaps?) be better ergonomically not to have to reimport Function.Definitions instantiated twice with _≈_...

[jamesmckinna]

See also #2581 for yet another variation on this theme...

[JacquesCarette]

About your two different Foo modules above: my impression was that, at the usage site, there are the same. So if they are not, that should warrant an explanation in the official documentation.

[jamesmckinna]

I'll refine the example to explain how I think they could be different at usage sites... returning to this now:

module Foo (p : P) where
  defn : ...
  defn = ...

can be imported (qualified or unqualified) two ways in client modules M:

• uninstantiated (as open import Foo as F), so that parameter p : P must be supplied explicitly at usage sites of F.defn in M (permitting distinct such instantiations, hence 'local')
• instantiated (as open import Foo p as F), so that p : P may be supplied globally once-and-for-all, but then all uses of F.defn implicitly take this single p (hence: 'global')

By contrast,

module Foo where
  module _ (p : P) where
    defn : ...
    defn = ...

can only be imported (qualified or unqualified) in the 'uninstantiated'/'local' way above.

So the first style seems both more ergonomically flexible, as well as extending that of the second in a compatible way.

As such, it seems preferable (cf. Algebra.Definitions, Algebra.Structures to adopt this style where possible (cf. #2572 , #2565 / #2567 ), although elsewhere (eg. #2397 ) there may be good reasons to enforce the 'local' style.

NB. the local/global distinction cashes out on import, but internal to a given module, the ergonomics work the other way round (that's the meaning of @MatthewDaggitt 's comments on #2397 IIUC)

[jamesmckinna]

Looping back to @Taneb 's OP, and mine and @MatthewDaggitt 's comments, there's a separate problem with 'too much' DRY-delegation of one hierarchy to another: the cognitive load on the user/reader in needing definitional equality to be 'transparent' across modules... it is, semantically, of course, but not 'visually'. Hence the recent discussion/critique of #2566 / #2581

[JacquesCarette]

Or more succinctly: mentally expanding definitions has non-zero cognitive load.

[Taneb]

Closing this, as I think it's been answered "we shouldn't do this even if we technically can" and the discussion has gone way further than I expected it would when I opened it.