In some cases, when the requirements of certain modules or module types are minimal, I have chosen to use (for example) CategoryDefinition parameters instead of depending on the full-blown Category interface.
In principle this makes the module/type functor "stronger": since it requires a smaller interface for its parameter it can be applied in more contexts. This was especially relevant when an Op : CategoryDefinition module was defined by CategoryTheory, at a point where it would have been impossible to give the full-blown Category type as that was still being defined and would be self-referential.
However, in practice it is unclear how often this will actually be beneficial and also makes things more complicated:
- more things come to depend on the specifics of
CategoryDefinition vs Category
- it may become necessary to rely on the full interface, breaking any code that relies on the
FooDefinition-only behavior;
- modules defined in terms of
CategoryDefinition cannot use the notations defined in CategoryTheory, and the code may be less readable as a result.
Because of this, we should probably move away from the practice of using FooDefinition parameters anywhere except for FooTheory and rare other places where the weaker dependency is required for a well-motivated reason.
In some cases, when the requirements of certain modules or module types are minimal, I have chosen to use (for example)
CategoryDefinitionparameters instead of depending on the full-blownCategoryinterface.In principle this makes the module/type functor "stronger": since it requires a smaller interface for its parameter it can be applied in more contexts. This was especially relevant when an
Op : CategoryDefinitionmodule was defined byCategoryTheory, at a point where it would have been impossible to give the full-blownCategorytype as that was still being defined and would be self-referential.However, in practice it is unclear how often this will actually be beneficial and also makes things more complicated:
CategoryDefinitionvsCategoryFooDefinition-only behavior;CategoryDefinitioncannot use the notations defined inCategoryTheory, and the code may be less readable as a result.Because of this, we should probably move away from the practice of using
FooDefinitionparameters anywhere except forFooTheoryand rare other places where the weaker dependency is required for a well-motivated reason.