Dear Sage developers,
This is a call for vote about the ticket:
#10963: axioms and more functorial constructions [1]
Sorry this post is long; it's trying to give a fair summary of the
huge discussion on [1]. Here is the table of contents:
- What is the ticket about
- Relevance
- History
- Debate
- Personal opinion
- Call for vote
What is the ticket about
------------------------
The main feature implemented by #10963 is an infrastructure for axioms
which enriches the current category infrastructure. Namely, if you
have a category, you can now ask for the (full) subcategory of the
objects satisfying a given axiom. For example:
sage: Groups().Finite()
Category of finite groups
Of course, this can be iterated:
sage: Magmas().Associative().Commutative().Unital().Inverse()
Category of commutative groups
By itself this is a little improvement, since it gives for example a
single entry point for all the variants of groups (or of magmas, ...);
in particular this will allow, as a later step, to remove a lot of
stuff from the global name space. This is in line with what we already
have for functorial constructions:
sage: Groups().CartesianProducts()
Category of cartesian products of groups
What's really new is that axioms play nicely with intersection:
sage: Groups() & Magmas().Commutative() & Sets().Finite()
Category of finite commutative groups
sage: (CommutativeAdditiveGroups() & Monoids()).Distributive()
Category of rings
sage: Rings().Division() & Sets().Finite() # Wedderburn's theorem
Category of finite fields
Fine, this is cute, but why is this relevant?
Relevance
---------
As time passes, the hierarchy of abstract classes for parents,
elements, and morphisms in Sage is getting larger and larger. From the
beginning, the purpose of categories in Sage has been to exploit the
strong semantic provided by the math to keep such large hierarchies
maintainable. The key is to fight hard against duplication and toward
single point of truth. Just as a trivial example, Sage deduces
automatically from the above that the abstract class for finite groups
(Groups().Finite().parent_class) should inherit from the abstract
class of groups and the abstract class of finite monoids.
Axioms are an important step to scale further by controling the
potential combinatorial explosion of the number of classes and
categories. For details, see the section on axioms in the primer [2].
History
-------
The work on this ticket started three years ago, growing up out of
strong immediate needs for the hierarchies of categories appearing in
the representation theory of semigroups or Hopf algebras. But the
infrastructure is also beneficial for non exotic categories like the
ones we have seen in the examples above. For example, it made it
practical to implement categories for the many variants of algebras
(unital or not, associative or not, commutative or not, ...)
For the design of the category infrastructure, we had some strong
source of inspiration from other systems like Axiom, MuPAD, or
Magma. As far as I know, no other system has a non trivial axiom
infrastructre like this one. Which means that it took a long time --
three years -- to analyse the needs, explore potential idioms, and
implement and reimplement the infrastructure until it felt right. It
also took as a prerequisite to fix a bunch of technical hurdles, in
particular #11935 and #13589 (thank you by the way to all who worked
and helped on those tickets, and in particular Simon and Nils).
In those three years, this ticket benefited from continuous
discussions with the other category fans, and in particular Florent
Hivert and Simon King. I also presented the framework at the occasion
of several Sage days to see how natural it would feel to new users and
developers. Most importantly, the framework was put to intensive use
in actual code to test whether the approach was sensible, viable, and
practical.
The undesirable consequence of this long history is that the ticket
has become large: it contains the axiom infrastructure, the
reorganization of the Sage categories using that infrastructure, a
bunch of new categories, and quite some related stuff that aggregated
to it along the way and would be painful to separate away (mostly
improvements to the existing functorial constructions).
Status
------
All test passes. The code is 100% doctested. All dependencies are
merged. Much time was spent on performance too, in particular checking
that the Sage startup time did not increase non trivially. Simon King
completely reviewed the code three months ago (thanks!!!) and gave a
positive review back then.
Since then, Simon, Nils, and Volker spotted and tracked down a bug
which is fixed now. I am super grateful to them because it was tricky:
the code was actually too paranoid! It did an assertion check too
early during some initialization, which caused a recursion loop
involving imports, and ended up with a silent garbage collection
issue.
This triggered a long discussion on trac where basically each and
every design choice was put again to trial, a good thing in itself!
Based on this discussion (thanks by the way to all the participants),
I added a 1500-lines overview text about axioms, including rationale
for the design decisions, the specification of the infrastructure, and
a detailed sketch of proof of correctness. This text, and some further
little improvements, are under review by Simon. There are also a few
further small suggestions from the reviewer's that I have offered to
implement, against my own opinion, if they really cared about
them. It's a matter of days before this is done.
This ticket is holding up a bunch of other tickets that depend on it,
either because they implement themselves new categories with axioms,
or use features from the ones implemented here. This includes:
- #14102: Non symmetric Macdonald polynomials. This is one of the main
outcomes of last year's ICERM semester. Up to one glitch that
appeared when merging with recent versions of Sage, it has been
ready to go since last June. It's an important feature and end users
are waiting for it.
- Work by PhD students (Jean-Baptiste Priez, ...) on Hopf algebras, a
large piece of which could go in very soon once #10963 is in. This
code is one of the major pieces of their PhD work, and they deserve
to get credit for it.
- #11111 and follow-ups on representation theory of finite dimensional
algebras and semigroups by Saliola, Aladin, Florent, myself, ...
- Further work on categories (support for morphisms, ...)
- A bunch of further stuff in the former Sage-Combinat queue
Taking this in consideration, since last June, basically all the
energy I could spend on Sage-development was devoted to finalizing
this ticket and getting it merged.
Debate
------
In my view, the most non obvious point about this ticket is whether
the general approach just makes any sense and is viable. De facto, it
took me three years to convince myself! Now I am convinced :-) And I
tried to be convincing in the documentation. Now, if you wonder about
this point, which is legitimate, actually sane, please read [2] and
decide for yourself. Comments and opinions are very welcome. Just
please create a new thread so that we don't mix the discussions.
As far as I can tell from the long trac discussion, there is a
reasonable consensus about this first point; I might be biased though.
There is also a consensus about a certain number of desirable further
features (see the TODO's in the documentation) that are best postponed
to follow-up tickets since this one is already way too large! One such
feature is to improve and make the overview text more concise, as it
matures thanks to the feedback from more and more developers reading
it.
Now, as often, there can be variants on how the approach is
implemented. And diverging opinions about those variants. Volker
dislikes some syntactical and implementation choices, and would like
to change some them. I dislike his counter propositions.
The difficulty in this discussion is that this is more about wild
guesses about the future; at this point, we lack concrete amo to back
up clear cut decisions; we just have forged different intuitions about
the right balances between different principles. That's fine by
itself: I like that developpers have opinions; it's a richness for the
Sage community. However we are stuck in an endless discussion with no
consensus emerging. And a lot of time is wasted on it when there is so
much else to do.
I think the divergence points are essentially about:
(1) The usage of nested classes: currently if Cs() is a category which
implements stuff for its subcategory Cs().A() of the objects
satisfying the axiom A, then that stuff is to be put in a class
Cs.A
Typically this class can be a nested class, or it can be put
elsewhere, e.g. in a lazily imported module, with a link from Cs;
this is very flexible.
(2) The "header" for categories with axioms
{{{
class Blah(Category):
# The currently implemented syntax
class Finite(CategoryWithAxiom):
...
# Volker's proposal, something like:
class ChooseYourName(axioms.Finite.Category):
...
}}}
plus possibly some attribute setting.
(3) Internal implementation points.
There is also a preexisting performance issue in some special
situations which is made worse by this ticket (see #15801). We have a
plan to fix it, and I am happy to settle this with Simon shortly after
#10963 is merged.
Personal opinion
----------------
About (1): we have been using the same syntax for functorial
constructions ever since the initial implementation of categories back
in 2009. It has proven a very practical way to structure the code, we
never had a problem with it, and developers learned it all right. I
don't see why we should deviate from this syntax for axioms given that
axioms are of the same nature as functorial construction, just with
more properties. If we decide for another syntax, then we should
change the syntax as well for functorial constructions. I am *not*
undertaking this change myself.
About (2): I had considered something similar earlier on, and
practical usage told me to drop it. In any cases, it's a rather small
change to the interface (one line or two per new category with
axiom). It can be implemented in a follow up ticket. Even in a couple
months there won't be hundreds of new categories with axioms
implemented out there. If we convince ourselves that we should really
change the interface, the categories with axioms in the Sage library
will be easy to fix. And we can warn and help the couple developpers
that will have implemented some in their private code.
About (3): the code is already functional. It certainly can be further
improved, but this can be postponned at no cost to followup tickets.
Conclusion: In such a situation where it comes to opinion against
opinion, I believe that decisions that have been battlefield tested
for sanity and practicality over a non trivial period (years) on a non
trivial body of code (50 categories just in the Sage library itself)
are as good as any other. The ticket is already way too big (I take my
share of the blame for it) and this is holding up the work of
many. Hence further development should go in follow up tickets,
especially if it's unclear whether they actually improve the
situation.
Let's not deviate even more from incremental development and the usual
"release early, release often".
Call for vote
-------------
[ ] Merge this ticket, and move on with further improvements in follow
up tickets
[ ] This ticket should be held up until everybody is happy
[ ] This ticket does not make any sense
Let me conclude by thanking everybody who has been involved in this
ticket. And also those who worked so hard on the new Sage development
workflow! It's been a life saver in the last months, and the previous
workflow has some responsibilities on the size of this ticket.
Cheers,
Nicolas
PS: I have tried hard to make a fair account of the situation. Yet
please read everything with a grain of salt, for this has been the
most frustrating development experience I ever had.
[1] http://trac.sagemath.org/ticket/10963
[2]
http://sage.math.washington.edu/home/nthiery/sage-6.0/src/doc/output/html/en/reference/categories/sage/categories/primer.html
--
You received this message because you are subscribed to the Google Groups
"sage-combinat-devel" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to sage-combinat-devel+unsubscr...@googlegroups.com.
To post to this group, send email to sage-combinat-devel@googlegroups.com.
Visit this group at http://groups.google.com/group/sage-combinat-devel.
For more options, visit https://groups.google.com/d/optout.
