Setoid parameter in algebra records

[mechvel]

May be it is better for standard library to improve the record design for algebra?
We wrote about this recently in the Agda list.

1. I complain on that (Magma.setoid +-magma) and (Magma.setoid *-magma) occurs not the same
   in Semiring. The same is for decSetoid. I do not find any better way out as introducing
   +-setoid and *-setoid in the application. And this does not look nice, it misleads the user.
2. James Wood wrote there about certain tricks to fix the effect.
3. I suggested (in the Agda mail list) the approach to improve the design, with attaching a piece
   of code.

Breaking backwards compatibility is not so bad at the current stage.
Because
a) so far, each new lib version still breaks almost all the user's application modules,
b) it is not difficult to port the application to a new version,
c) each application specifies the needed Agda version (and hence the lib version),
install this version and enjoy,
Probably, we need to continue this way until it becomes stable in somewhat a natural way.

[JacquesCarette]

The problem here is one of sharing: there is a Setoid that appears twice, but should really only appear once, structurally.

One way to deal with it is via having both bundled and unbundled versions of some structures. That way the sharing can be expressed via parameters instead of fields. The drawback is that even though the bundled and unbundled versions are semantically equivalent, Agda doesn't know that, and so 'work' needs to be done to go back and forth. [In theory, cubical solves this, but I am not convinced if this is yet true in practice.]

Note that the Arend theorem prover has solved this problem really nicely already. And its solution seems very Agda-compatible to me. The Agda developers are aware of this, but they may not yet be aware of the impact it has on the current library development.

[mechvel]

A simple and natural solution is needed.
My suggestion is concrete.
A small sample code is attached here as
Structures.agda.zip
to demonstrate the approach.
IsMagma is parameterized by Setoid,
(Semigroup is skipped here, for a contrived example),
IsSemiring is parameterized by Magma, which is taken as +-magma, and the items for * are
tied there to (Magma.setoid +-magma) . And Semiring.*-magma is formed over this setoid,
not as field, but as a value.
And so on.
I think the `base' setoid is unique in this design. Is it?
Is not all this natural and simple?
What people think of this?
May be this approach is well-known, all right, but can the library be fixed this way?
May be this implements of what you call "sharing can be expressed via parameters instead of fields", but it is a concrete version of this general idea. The details do matter.

[mechvel]

For any occasion: if the approach occurs all right, I do not pretend for authorship. Probably the approach is well-known, besides, the idea is evident to everyone. The matter is that the library needs to be fixed in somewhat a natural and sensible way. And I doubt about what can be this way.

[jespercockx]

This is a recurring problem in most proof assistants and has been studied extensively in the past, for example by Gontier et al. (https://hal.inria.fr/inria-00368403v2) for their formalization of the Feit-Thompson Theorem in Coq. This paper gives a rather nuanced view on the tradeoffs between the bundled and unbundled representation of algebraic structures. Their recommendation is to define structures as small components ('mixins') that can be composed freely in record types. They also rely heavily on type-classes in Coq to fill in missing parts of those record types. In Agda the equivalent would be to use instance search (though the standard library has thus far -- quite understandably -- refrained from using those). They also rely quite a lot on implicit coercions, which does not (yet) have an equivalent in Agda.

[mechvel]

Before considering wise theories it has sense to check the simplest way out.
What is wrong in the approach of Structures.agda.zip ?

[jespercockx]

Your design looks reasonable to me, but the problem is that there are many possible designs that all look reasonable, and the disadvantages of a certain approach do not appear until one is 9 levels deep in a hierarchy of algebraic structures (this is the point made in the paper).

One concrete problem that could happen with your proposal is that later on you have a similar problem, not for Setoid but for a different structure (e.g. Group): a CommutativeSemiring and a IdempotentSemiring both share the same underlying Group for the addition and multiplication, but when both of them are used together Agda will again not see that they are equal. Then you have to parametrize IsCommutativeSemiring and IsIdempotentSemiring by a group instead of a setoid.

My point is not that these problems are impossible to solve, but rather that there are many choices to be made and their effects are not apparent until much later. So if we do not want to waste a lot of time trying out these possibilities, we might want to look at what others have learned about the problem.

[mechvel]

but the problem is that there are many possible designs that all look reasonable, and the
disadvantages of a certain approach do not appear until one is 9 levels deep

Sounds reasonable.

One concrete problem that could happen with your proposal is that later on you have a similar
problem, not for Setoid but for a different structure (e.g. Group): a CommutativeSemiring and a
IdempotentSemiring both share the same underlying Group for the addition and multiplication,
but when both of them are used together Agda will again not see that they are equal. Then you
have to parametrize IsCommutativeSemiring and IsIdempotentSemiring by a group instead of a
setoid.

I have a hope that this would not happen. Because IsCommutativeSemiring has to be parameterized by Semiring rather than Setoid or Group
(I do not see IsIdempotentSemiring in lib, probably you example is contrived).
Generally, in the suggested design, Is<Structure> is parameterized by <predecessor-Structure>
(Setoid occurs a parameter only when <Structure> is Magma).

To test the approach, one needs, may be, to set these 9 levels of definitions, and to provide a program that checks all places where such a uniqueness is needed, and to see whether it is type-checked.
May be the approach of Structures.agda.zip is sufficient, and can be checked this way.
But I am not sure.

May be indeed, it is needed to study the works like the paper you refer.
Personally I am not ready to start a systematic study of the subject right now.
And meanwhile, settting +-setoid and *-setoid to user program looks awful.

[mechvel]

I wrote

To test the approach, one needs, may be, to set these 9 levels of definitions, and to provide a
program that checks all places where such a uniqueness is needed, and to see whether it is type-
checked.
May be the approach of Structures.agda.zip is sufficient, and can be checked this way.

Jesper (and anyone),
can you provide a counter-example to the approach of Structures.agda.zip ?
Then I would test such by extending the code along the hierarchy -- if it will not be too large.

[mechvel]

For any occasion:
if the team ever considers parameterizing algebra hierarchy by Setoid,
then prepare to that there are many usable domains of two or may be three setoids.
For example a left module over a ring R: coefficients live in R, vectors live in an Abelian group over a setoid S, and S often occurs very different from the setoid of R.

[MatthewDaggitt]

As @jespercockx says, it's impossible to know where the downsides of your approach would lie without trying it out in large scale developments. In order to make this change, I'd want to see a significant proof of concept. Translating the standard library to use it would be the absolute minimum.

However, there's also a cost-benefit analysis to consider. This is not a minor change you're proposing, but will require everyone to entirely rewrite all of their algebra related code. I 100% agree with you that the current situation is not ideal but currently as I understand it your main argument for the change is that:

And this does not look nice, it misleads the user.

meanwhile, settting +-setoid and *-setoid to user program looks awful.

Unfortunately we would need a better reason than that to break everyone's code so completely. Is there anything you can't do with the current design?

[JacquesCarette]

This problem is really hard: think of being able to easily express that a field is a 1-dimensional vector space over itself, fully sharing the underlying Setoid (and more). Vector spaces are naturally 'very' 2-sorted, but sometimes you need to know things definitionally.

The current library design has its flaws, for sure. But there is no point going to another, potentially somewhat better, design if we already know that it too won't scale. You don't want to massively break people code's twice.

A proper library contains hundreds of 'diamonds' - see Library/mathscheme.tog in https://github.com/ysharoda/tog. [For the curious, those 315 lines of code actually mean 22000 lines in raw tog, which is basically a cut-down Agda, see Library/mathscheme-generated.tog].

[mechvel]

This problem is really hard: think of being able to easily express that a field is a 1-dimensional
vector space over itself, fully sharing the underlying Setoid (and more).

This example is easy. I have 3-4 page program presenting an approach to fix standard library.

• OneBaseStructures.agda defines the hierarchy from Magma to CommutativeRing.
• OfModuleOver-I.agda defines left module over a ring, this has 2 setoid parameters.
  It also defines AssociativeAlgebra over a CommutativeRing. It extends the above LeftModule
  with the vector multiplication, so that vectors form a Ring of their own.
  It includes the two rings over different setoids, related in a certain way.
• OfRing-II.agda implements the instance of LeftModule where any ring R is a module over
  itself. This module has only 18 non-empty lines.
  The above sharing is expressed by repeating the parameter setoid in the declarations

module OfRing-II {α α=} (setoid : Setoid α α=) where
open OneBaseStructures setoid using (Ring)       
open OfModuleOver-I setoid setoid using (IsLeftModule; LeftModule)

Then the goal is declared as ringAsLeftModule : Ring → LeftModule.

I do not believe that people would agree to essentially refactor the library.
But there needs to be an idea of a really adequate library, and a piece of code of, say, 10 pages
representing this idea.
And currently we have not such an idea.
In particular, I am not sure that these my 4 pages present a really adequate approach.

[mechvel]

And this does not look nice, it misleads the user.

meanwhile, settting +-setoid and *-setoid to user program looks awful.

Unfortunately we would need a better reason than that to break everyone's code so completely. Is > there anything you can't do with the current design?

Everything algorithmic can be expressed in almost any language.
I search for a language in which mathematical computations can be set in a possibly more adequate form, in a possibly nice way.
I think that Agda cares of this adequacy more than other languages.
If it really cares of this, then it needs to allow the code refactoring more easily than it is in other systems. Because it has a chance to converge to an adequate design.

Still I do not think that the above my note about the two setoids is sufficient to immediately start to change the library.
But someone needs to develop the idea, and to prove it.
May be there needs to be developed new standard base algebra (only the algebra part),
so that people could test of whether it is more adequate than lib-1.3.

[mechvel]

think of being able to easily express that a field is a 1-dimensional vector space over itself, fully
sharing the underlying Setoid (and more).

Vector spaces are not in standard library. This is a subject of applied libraries.
But (Agda + standard library) needs to be an adequate tool for the programmer to define and implement VectorSpace and its related items.
I tried things like VectorSpace, and further, AssociativeAlgebra over a commutative ring.
The only spot I met so far is this case of unneeded relevance of setoid (in Semiring).

For any occasion: there is another area where (Agda + standard library) is tested:
substructures. These are sub-magma ... sub-group ... sub-ring ... Ideal in a ring.
For example, in any IntegralRing R, the subset of non-zero elements forms a monoid by multiplication, and this monoid is not the same as *-monoid of R.
Even numbers form a group which is a sub-group of Integer by _+_.
A substructure can be expressed in Agda by a membership predicate (with adding the corresponding
axioms). Sometimes it can be (algorithmically) defined by a set of generators.
This is also a field to test the adequacy of the type system: how nicely will it express the known algebraic constructs.

[JacquesCarette]

'substructures' are a very set-theoretic notion. They do not mesh very well with type theory. This is why in Coq (in mathcomp) and I think now Lean too, 'sub' structures per se do not exist. What you do have are structures also injective homomorphisms (usual substructures assume the underlying function of the homomorphism is the identity function; this is an over-constraint inherited from set-thinking).

Some known algebraic constructs turn out to 'bake in' stuff from foundations that people had not realized until they tried to formalize them in other foundations. George Gonthier (and many co-authors) have written multiple times about this. There was a long twitter thread with Andrej Bauer and Kevin Buzzard 'unraveling' these ideas too.

Expressing 'substructure' via a membership predicate (that is the forgotten at point of use) works, but turns out to be a hack, that ports set-thinking over to type theory. This is not stable under various natural operations. So it should not be regarded as a good encoding of the mathematical notion.

[mechvel]

Expressing 'substructure' via a membership predicate
[..]
should not be regarded as a good encoding of the mathematical notion.

Consider a simple example. One has to implement in Agda the following discourse.
"Let M be a magma with carrier Carrier and the operation ∙.
A magma M' with Carrier' and operation ∙' is called a submagma in M if and only if
Carrier' is a subset in Carrier closed under the operation ∙,
and ∙' is a restriction of ∙ onto Carrier'.
Lemma. If M' is a submagma in M, and M is commutative, then M' is commutative.
Proof: ...
"
I define a subset of Carrier by

module Substructures {α α≈ p} (setoid : Setoid α α≈) (open Setoid setoid)
                      (Member : Pred Carrier p)  (respM  : Member Respects _≈_)
                      where
Carrierₛ : Set _ 
Carrierₛ = Σ Carrier Member    -- a subset of Carrier defined by a predicate  

Then it is easy to define the equality =ₛ induced by ≈, ∙ₛ induced by ∙,
and to prove the above lemma, and many other needed things.
What is evil in this approach?

Well, one can define this as an injective homomorphism from M' to M (agreed with the two equality relations). And the above lemma also is easy to prove.
But

• this is not as close to the original mathematical definition,
• for example, the subset of even integer numbers is easily expressed as Σ ℤ IsEven,
  while implementing the needed injection does not look so nice, because one needs to define the
  domain of this map.

But the main question for me is: what precisely is evil in the approach with a predicate?
(the subject is easier to understand when it its given a simple example).

If you are going to explain the subject, then it is probably better to open another issue. For example,
"Substructures".
Thanks.

[JacquesCarette]

I completely agree that it is not as close to the original definition! The point is that maybe the original definition was sub-optimal.

The approach with the predicate is not 'evil'. It seems to not scale: later theorems will want a Group, not a Subgroup, as input (for example). The other thing is that "change of variables" (representation, etc) doesn't necessarily transport the predicate the way you want it to. To insure that it does, you need various preservation lemmas. [That's the whole point of Setoid, for other parts of preservation.] Those preservation properties are usually trivial, which is why you never encounter them in classical mathematics. But classical mathematics is sloppy, and gets tripped up when a usually-trivial lemma turns out to be difficult.

They're having difficulties in Lean with certain things having to do with localization (of groups) because of that.

[mechvel]

The approach with the predicate is not 'evil'. It seems to not scale: later theorems will want a
Group, not a Subgroup, as input (for example).

If Σ ℤ IsEven does not scale, then what does scale? To apply a homomorphic injection, what can be the carrier of this injection, is it again Σ ℤ IsEven ?

later theorems will want a Group, not a Subgroup, as input (for example).

record Subgroup ... is parameterized by baseGroup : Group.
it implements various items describing the relation between baseGroup and the subgroup.
And it also forms and exports subgroup-asGroup : Group as a stand-alone group.
This thing is trivial. So that for later theorems you write of, the program has to extract
(Subgroup.subgroupAsGroup foo)
(if only I understand of what you are writing about).

The other thing is that "change of variables" (representation, etc) doesn't necessarily transport
the predicate the way you want it to.

For example, integer numbers are represented in unary system (ℤ). One can consider ℤb -
for the binary system. Having the isomorphism toBin : ℤ -> ℤb, and the subgroup for
Σ ℤ IsEven, we can build the Subgroup record describing of the image of this subgroup.
Its carrier is expressed by a certain predicate IsEvenBin : Pred Bin _, and one has to prove that the first carrier is bijected to the second one by toBin. This all looks natural, and easy to arrange. What does not scale here, I wonder.
(again, if only I understand your note).

[JacquesCarette]

The carrier is whatever you want, as long as it's isomorphic to the even integers.

The problem with nesting records has been well-documented - See Type Classes for Mathematics in Type Theory as a particularly lucid explanation. It's not that it doesn't work, it's that it only works in simple cases.

Again, for transport, the problem is not that it doesn't work - it works quite well for simple cases. You can see some examples of this breakdown in the (very recent) preprint Formalizing functional analysis structures in dependent type theory.

[MatthewDaggitt]

@mechvel I'm going to close this and similar issues as the consensus of people far more informed than I appears to be that this is a language design problem, not a library design problem.