Refactoring: expressing bigger theories in terms of smaller ones

[gallais]

Riffing off #12 (comment)

This is what I came up with with a very basic Semigroup & Monoid example rather than
the bigger one involving Ring:

||| Inclusion of one signature into another.
-- Do we already have this somewhere?
public export
OpMorph : (p, q : Signature) -> Type
OpMorph p q = {n : Nat} -> p .OpWithArity n -> q .OpWithArity n

Semigroup is what you'd expect. Notice that I have lifted axiom to the
toplevel instead of having MkPresentation _ _ $ \case (...) and that it
takes an OpMorph as an argument: if you can make sense of a semigroup's
operations in a larger context then you can make sense of its axioms too.

||| The syntax and axioms for semigroups
module Frexlet.Semigroup.Theory

import Frex

public export
data Operation : Nat -> Type where
  Product : Operation 2

public export
Signature : Signature
Signature = MkSignature Operation

public export
data Axiom
 = Associativity

public export
axiom : {sig : _} -> OpMorph Signature sig -> Axiom -> Equation sig
axiom interp Associativity = associativity (interp Product)

public export
SemigroupTheory : Presentation
SemigroupTheory = MkPresentation Theory.Signature Theory.Axiom (axiom id)

And this is the refactored Monoid.Theory. Notice how theSemigroup is
used to focus on Product only out of all the operations.

||| The syntax and axioms for monoids
module Frexlet.Monoid.Theory

import Frexlet.Semigroup.Theory as Semigroup
import Frex

public export
data Operation : Nat -> Type where
  Neutral : Operation 0
  Product : Operation 2

public export
Signature : Signature
Signature = MkSignature Monoid.Theory.Operation

public export
data Axiom
 = LftNeutrality
 | RgtNeutrality
 | Semigroup Semigroup.Axiom

theSemigroup : OpMorph Semigroup.Signature Monoid.Theory.Signature
theSemigroup Semigroup.Product = Monoid.Theory.Product

public export
axiom : {sig : _} -> OpMorph Monoid.Theory.Signature sig ->
        Monoid.Theory.Axiom -> Equation sig
axiom interp LftNeutrality  = lftNeutrality (interp Neutral) (interp Product)
axiom interp RgtNeutrality  = rgtNeutrality (interp Neutral) (interp Product)
axiom interp (Semigroup ax) = Semigroup.axiom (interp . theSemigroup) ax

public export
MonoidTheory : Presentation
MonoidTheory = MkPresentation Monoid.Theory.Signature Monoid.Theory.Axiom (axiom id)

Is this the kind of stuff you had in mind @ohad?

[ohad]

This example is a bit degenerate, but roughly. I would also try to re-use the operation Product rather than duplicate it like we do in the code snippet.

Semigroup is a little different than semiring because we're adding to the single binary operation.
In a semiring, I would try to have two copies of a semigroup (additive and multiplicative), both for the operations and the axioms, and then only add the interaction laws between them.

You're right that there might be other ways to organise the data, both in terms of operations and in terms of axioms, and that using one way might bias the structure against another one, while a flat representation for the operations and types is going to be unbiased. But I worry that this unbiased approach would make all developments equally miserable, rather than making some things easy, and some things hard.