Drop equivalence relation from Algebra.Bundles.Raw structures?

[carlostome]

Structures currently defined in Algebra.Bundles.Raw (RawMagma, RawMonoid,...) include as part of their definitions the "underlying equality" relation. For example,

record RawMagma c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier

The rationale behind Raw structures (cf. README.Design.Hierarchies) seems to be that they ought to only bundle algebraic operations (e.g. _∙_ : Op₂ Carrier above) in a spirit similar to Haskell's typeclasses.

Wouldn't it make sense to drop the _≈_ relation from these structures?

As a point of comparison, the Raw structure for functor does not include such relation (Effect.Functor):

record RawFunctor (F : Set ℓ → Set ℓ′) : Set (suc ℓ ⊔ ℓ′) where
  infixl 4 _<$>_ _<$_
  infixl 1 _<&>_
  field
    _<$>_ : (A → B) → F A → F B
  ...

[Taneb]

We're using the _≈_ in the raw algebraic structures to define the laws of homomorphisms. We can't easily remove it.

[carlostome]

Why are these part of the structures as opposed to being parameters of homomorphism?

[jamesmckinna]

Thanks @carlostome for the (challenging!) questions. I hope the rambling discussion below helps...

I'd make two observations before going away to try to think a bit harder about this (and probably nudge @JacquesCarette and @MatthewDaggitt for comment...):

• I think the comparison with (Raw)Functor is problematic, or at least, not immediately applicable, precisely because the design there has always foundered on the difficulty of how to capture, in general, the 'right' notion of equality on arbitrary F A in order to be able to correctly formulate the laws...; by contrast, within a given algebraic structure, the 'parameter' wrt which the algebraic laws are formulated, namely _≈_ is readily captured; but for all that, it is still a design choice as to whether you include equality as part of the 'raw' signature or not, and @Taneb makes one argument for it (all design choices eventually come down to such pragmatics in the end?)
• regarding parameterisation, for sure we could have completely unbundled parameter telescopes everywhere (a meta-design principle of minimum commitment), and indeed we still see vestiges of this in the long telescopes associated with the Algebra.Structures.IsX structures... so much so that I have argued against the current design, in favour of making (a version of) the Raw bundles as a single parameter to the IsX structures in [DRY] Reconciling the indices of IsX with those of the corresponding RawX #2252 , and there, I don't think it would make sense to omit the relation, precisely because the specification of laws requires the relation... (my only point of divergence would be to make the underlying {A : Set a} be a parameter to Raw bundles, rather than an explicit field... there's a separate discussion to be had there about 'sharing by parametrisation'/'Pebble-style' sharing which, though relevant here, is a bit too wide a scope for your questions, I think?)

For better or worse (and certainly, pre the development of HoTT/cubical ideas around making equality a global/ambient property of types), stdlib makes the choice ('Bishop-style'?) of a (pre-)Setoid-based organisation of the library design of all/most of the basic abstract objects in the library. Changing that now would be... a major undertaking, and a significant fork in the design space.

The (not an exact one, though!) analogy from universal algebra (I think! UA experts please correct me if not) is whether or not equality is taken as explicit part of the relational signature, or presupposed. Making equality part of the Raw bundle is (a version of) the 'presupposed' design choice.

The 'dirty' reason underlying such a choice is precisely (?) to avoid marshalling and unmarshalling an explicit (Raw)Setoid object underlying any given algebraic structure (or correspondingly at any higher level of abstraction), with all the space+time complexity disadvantages that would entail. In an ideal implementation, such marshalling/unmarshalling would be cost-free (@JacquesCarette has looked at this extensively with his students, and it's implemented, IIUC, in the Arend system) but that is not, alas, where we are with Agda.

Lastly, I'm always reluctant to take too seriously any comparison with haskell typeclasses, precisely because, by not having to take laws seriously, they avoid all the hard work in figuring out a workable design for 'real' algebraic structure (never mind the compromises entailed by having type-checking based on (unique) instance inference...)

[jamesmckinna]

Under propositions-as-types, I'd be tempted to go out on a limb and say that the 'operational signature' ('syntax') of an algebra includes/should include the 'relational signature', since together they define the language in which the equations ('semantics') can be stated as properties expressed relative to such a vocabulary... but that's probably a reach too far, philosophically at least?

After all, the ordered structures under Relation.Binary take their equality and ordering symbols as parameters to the IsX structures... although as we don't yet have Raw versions of the corresponding bundles #2491 its not a fair comparison ...

TL;DR: I think the orthodox first-order model theory distinction between function symbols and relations is artificial, just as is that between 'expressions' and 'terms' as to well-formedness wrt a possibly non-context-free grammar.

[jamesmckinna]

And... finally: what would we do if we went beyond purely first-order algebraic signatures to essentially algebraic, where equality plays a role in even defining well-formedness of terms (eg specifying pullbacks as a 'function' of conical data)?

[MatthewDaggitt]

My feeling is that, yes, there is a possible argument for removing the equality parameter from the raw bundles, but that in practice to do so would be an unavoidably huge breaking change. As has been mentioned by @jamesmckinna passing the equalities as arguments would also result in extra friction so the motivation for doing so would have to be strong.

Is there something that you concretely can't do with the current setup?

[JacquesCarette]

There are indeed multiple coherent designs here. The current one seems to be a rather good compromise between an ideal design (that would make as many things as possible independent) and one that works with "today's Agda". @jamesmckinna lays out the possibilities quite well.

I don't think that just dropping these equivalence relations would land us at a 'better' design (and certainly would break tons of code). I think a 'better' design that the current one would require significantly more changes [and some Agda support.]

[jamesmckinna]

@carlostome would you prefer to keep this open, or can/should we close now, against the possibility of re-opening in the future?

[carlostome]

Thanks everyone for the enlightening replies. After reading through the comments, I realize that including the equality relation aligns best with the overall organization of the standard library around Setoids.

I think we can close the issue.

[jamesmckinna]

@carlostome writes:

I think we can close the issue.

I do too, but it (and most importantly, the discussion above!) will happily remain part of the (long, and hopefully eventually, storied) history of stdlib.

Thanks for your question and thoughtful response to our feedback,