categories

[Bill Page]

[Changed thread subject from: Sources of funding - perhaps computer
manufacturers? ]

What I find hard to swallow is the peculiar mix of "parent",
"category", and Python data types (class system and inheritance). In
spite of the available documentation in the category system in Sage, I
really don't know what to use when and how to map it properly to
abstract mathematics in such a way as to gain as much as possible from
the existing Sage libraries. The situation is very different in
Axiom/Aldor.

It is good that you mention Aldor because it was designed specifically
as the "next generation" of Axiom library compiler but for entirely
non-technical reasons never achieved this status. On the other hand
the Aldor documentation is still the best available documentation of
the Axiom type system.

http://www.aldor.org/docs/aldorug.pdf

Aldor is currently supported only by the FriCAS fork of Axiom. Aldor
development itself is not dead, merely sleeping, and apparently a low
priority for the several people involved.

https://github.com/pippijn/aldor

To the best of my knowledge the Sage-combinat development of the
category system in Sage was motivated largely by the experience of
some of the developers with the Axiom-like category system that was
implemented in MuPad. MuPad was originally modeled after an early
version of Maple and so far as I know has a syntactic/symbolic
orientation at it's core (like Maple, Mathematica and Maxima) rather
than a more "algebraic" one. The MuPad developers borrowed from Axiom
in developing a more static type-oriented architecture for the
library. Maple itself as you might know has taken a rather different
approach. But in any case, compared to Axiom, the MuPad category
systems seems to me to be more or less grafted-on. And the Sage
category system seems much more so.

The little that I know about the Julia type system, mostly from
discussions about Axiom and Aldor on that mailing list about a year
ago, is that it has a more malleable design that one might expect to
enable a more integrated implementation of the central ideas of the
Axiom category system. So far as I know however no one is working on
this specifically.

---

I am happy to continue the discussion of Axiom, Aldor and FriCAS but I
am not sure if this discussion is entirely appropriate the the
sage-devel list. Is there a Julia/Nemo list where this should be
continued?

Regards,
Bill Page.


On 1 October 2015 at 10:56, Bill Hart <goodwi...@googlemail.com> wrote:
>
> On Thursday, 1 October 2015 16:35:20 UTC+2, Bill Page wrote:
> <SNIP>
>>
>> Unfortunately while I am very much in favor of the category/domain
>> approach of Axiom and related systems, I find the Sage implementation
>> of this idea almost entirely indigestible. Perhaps this is not the
>> case for a sufficiently large number of potential Sage developers.
>
> Bill, I would be very interested if you could elaborate on this point in
> more detail (assume I don't know anything about Aldor/Spad because it is so
> long ago that I read the manual for Aldor that I really have forgotten how
> this works over there).
>
> I'm currently implementing a system in Julia which really follows the design
> of Sage's parent/element setup quite closely (we tried another approach, but
> it failed). Since the project I'm working on is yet very young, I'd like to
> understand what is unpalatable about the Sage approach, since I'm
> essentially using it.
>

[William Stein]

On Thu, Oct 1, 2015 at 9:38 AM, Bill Page <bill...@newsynthesis.org> wrote:
> [Changed thread subject from: Sources of funding - perhaps computer
> manufacturers? ]
>
> What I find hard to swallow is the peculiar mix of "parent",
> "category", and Python data types (class system and inheritance). In
> spite of the available documentation in the category system in Sage, I

Just curious -- Bill Page, did you ever take a graduate mathematics
course in "category theory", or at least a course that had a
significant portion devoted to it, or at least carefully read (and did
exercises!) from a textbook on category theory? Because despite
being called "abstract nonsense" by some, category is a serious,
highly technical, and nontrivial area of mathematics, with interesting
theorems, a long development, etc., just like other areas of math.

I would expect that somebody who doesn't know category theory (the
mathematical area) would find the category framework in Sage very
confusing, just like somebody who doesn't know calculus might find the
symbolic functionality confusing.

-- William

> --
> You received this message because you are subscribed to the Google Groups "sage-devel" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+...@googlegroups.com.
> To post to this group, send email to sage-...@googlegroups.com.
> Visit this group at http://groups.google.com/group/sage-devel.
> For more options, visit https://groups.google.com/d/optout.



--
William (http://wstein.org)

[Bill Hart]

Thanks for the quick reply Bill.

Your comments make more sense (to me) now, since I see that your concerns are more about the way categories are handled in Sage, or at least how it interacts with the parent/element system.

At this stage there is no category theory in Nemo (it wouldn't be appropriate in Julia itself, since that is a general purpose language, not really a CAS).

There is a Nemo development list by the way. It's nemo-devel on Google Groups. It's public, so anyone can request to join.

If you prefer to discuss it further there, you are most welcome. Though I must warn that Nemo is a very new system and there are no efforts started or planned for category theory.

Nemo isn't trying to be the next Sage, so it's not even clear that thinking about categories in Nemo is even meaningful. Nemo exists primarily to do something innovative for that part of computer algebra/number theory that requires very fast generics. That doesn't really cover category theory I don't think.

However, our group in Kaiserslautern is good friends with the group in Achen doing HomAlg and Cap, which are category theory projects making use of Gap 4. There may be some interaction between us and them in the future, since at the very least we plan to interface with Gap.

Bill.

[Dima Pasechnik]

On Thursday, 1 October 2015 10:32:43 UTC-7, Bill Hart wrote:

Thanks for the quick reply Bill.

Your comments make more sense (to me) now, since I see that your concerns are more about the way categories are handled in Sage, or at least how it interacts with the parent/element system.

At this stage there is no category theory in Nemo (it wouldn't be appropriate in Julia itself, since that is a general purpose language, not really a CAS).

There is a Nemo development list by the way. It's nemo-devel on Google Groups. It's public, so anyone can request to join.

If you prefer to discuss it further there, you are most welcome. Though I must warn that Nemo is a very new system and there are no efforts started or planned for category theory.

Nemo isn't trying to be the next Sage, so it's not even clear that thinking about categories in Nemo is even meaningful. Nemo exists primarily to do something innovative for that part of computer algebra/number theory that requires very fast generics. That doesn't really cover category theory I don't think.

However, our group in Kaiserslautern is good friends with the group in Achen doing HomAlg and Cap, which are category theory projects making use of Gap 4. There may be some interaction between us and them in the future, since at the very least we plan to interface with Gap.

One probably can do a Julia interface to libGAP relatively easily.

Did you look into this?

Dima

[Bill Page]

On 1 October 2015 at 13:07, William Stein <wst...@gmail.com> wrote:
> On Thu, Oct 1, 2015 at 9:38 AM, Bill Page <bill...@newsynthesis.org> wrote:
>> [Changed thread subject from: Sources of funding - perhaps computer
>> manufacturers? ]
>>
>> What I find hard to swallow is the peculiar mix of "parent",
>> "category", and Python data types (class system and inheritance). In
>> spite of the available documentation in the category system in Sage, I
>
> Just curious -- Bill Page, did you ever take a graduate mathematics
> course in "category theory", or at least a course that had a
> significant portion devoted to it, or at least carefully read (and did
> exercises!) from a textbook on category theory?

Yes, yes, and yes.

> Because despite
> being called "abstract nonsense" by some, category is a serious,
> highly technical, and nontrivial area of mathematics, with interesting
> theorems, a long development, etc., just like other areas of math.
>

Yes, certainly. I consider category theory an appropriate foundation
for a very large part of mathematics.

> I would expect that somebody who doesn't know category theory (the
> mathematical area) would find the category framework in Sage very
> confusing, just like somebody who doesn't know calculus might find the
> symbolic functionality confusing.

No, I find the Sage implementation of these ideas confusing, or at the
very least overly complicated. I am sure that if I had a good reason
and enough energy to want to overcome this impression
(pre-conception?) then I would probably find categories in Sage very
useful. It certainly seems to be useful to at least a small core of
developers in Sage.

It is important also to keep in mind what are called "categories" in
Axiom have a best only an indirect connection to mathematical category
theory. To my knowledge there has been only a bit of work done in
trying to actually implement some form of category theory in
Axiom/Aldor.

http://axiom-wiki.newsynthesis.org/CategoryTheoryAndAxiom

[William Stein]

Cool; thanks for explaining your background.

One other impression you have is that categories were just bolted on
by combinatorics people at the end. However, David Kohel and I
actually implemented the first round of category-related stuff in Sage
right at the very, very beginning -- it was one of the first things we
did, motivated by what David had wished Magma had. And it is has
just been iteratively refined over the users, with Nicolas Thiéry
doing by far the most work on it during his sabbatical a few years
ago. There was also a lot of input coming from the multiple rounds
of rewriting of the coercion model, by me, David Roe, Robert Bradshaw
(especially), and others.

By the way, look at how coercion "works" in Magma:

$ magma
Magma V2.18-5 Thu Oct 1 2015 16:59:12 on compute3-us [Seed = 629019987]
Type ? for help. Type <Ctrl>-D to quit.
> R<x> := PolynomialRing(IntegerRing());
> x + 1/2;

>> x + 1/2;
^
Runtime error in '+': Bad argument types
Argument types given: RngUPolElt[RngInt], FldRatElt

>

Total time: 0.550 seconds, Total memory usage: 9.53MB

-- William

>
> It is important also to keep in mind what are called "categories" in
> Axiom have a best only an indirect connection to mathematical category
> theory. To my knowledge there has been only a bit of work done in
> trying to actually implement some form of category theory in
> Axiom/Aldor.
>
> http://axiom-wiki.newsynthesis.org/CategoryTheoryAndAxiom
>

[Bill Page]

On 1 October 2015 at 14:23, William Stein <wst...@gmail.com> wrote:
> ...

> One other impression you have is that categories were just bolted on
> by combinatorics people at the end. However, David Kohel and I
> actually implemented the first round of category-related stuff in Sage
> right at the very, very beginning -- it was one of the first things we
> did, motivated by what David had wished Magma had.

The concept of "parent" is adopted from Magma, right? I am not sure I
really understand it, either relative to the usual inheritance rules
in Python or category theory. Clearly the related? concept of
"element" is borrowed from category theory - maybe even topos theory?

Is there a reasonably short description of categories in Sage "for
category theorists"?

> And it is has
> just been iteratively refined over the users, with Nicolas Thiéry
> doing by far the most work on it during his sabbatical a few years
> ago. There was also a lot of input coming from the multiple rounds
> of rewriting of the coercion model, by me, David Roe, Robert Bradshaw
> (especially), and others.
>

Do you consider the coercion model as part of or motivated by category
theory in Sage?

There was some early work on this in Axiom, e.g.

http://dl.acm.org/citation.cfm?doid=309831.309944
Automated coercion for axiom
by Nicolas J. Doye

also his thesis:
http://axiom-wiki.newsynthesis.org/public/refs/doye-aldor-phd.pdf

but for the most part I would say that Axiom does not actually
implement coercion in this way.

[William Stein]

On Thu, Oct 1, 2015 at 12:00 PM, Bill Page <bill...@newsynthesis.org> wrote:
> On 1 October 2015 at 14:23, William Stein <wst...@gmail.com> wrote:
>> ...
>> One other impression you have is that categories were just bolted on
>> by combinatorics people at the end. However, David Kohel and I
>> actually implemented the first round of category-related stuff in Sage
>> right at the very, very beginning -- it was one of the first things we
>> did, motivated by what David had wished Magma had.
>
> The concept of "parent" is adopted from Magma, right? I am not sure I
> really understand it, either relative to the usual inheritance rules
> in Python or category theory. Clearly the related? concept of
> "element" is borrowed from category theory - maybe even topos theory?

Yes, parents and elements are from Magma. To me they have nothing to
do with category theory. Category theory is one level up, and is
about abstracting away from thinking about parents and elements (and
instead thinking about objects, morphisms, and functors). Just as
Bill Hart said, the parent/element approach in magma is very useful,
and inspired Sage and Nemo, but isn't category theory.

> Is there a reasonably short description of categories in Sage "for
> category theorists"?

No idea....

>
>> And it is has
>> just been iteratively refined over the users, with Nicolas Thiéry
>> doing by far the most work on it during his sabbatical a few years
>> ago. There was also a lot of input coming from the multiple rounds
>> of rewriting of the coercion model, by me, David Roe, Robert Bradshaw
>> (especially), and others.
>>
>
> Do you consider the coercion model as part of or motivated by category
> theory in Sage?

Yes, very much so -- that's the part I worried about more. Though
another motivation is for category theory is better code sharing
(that's more of the part that Nicolas added).

-- William


--
William (http://wstein.org)

[Bill Hart]

On 1 October 2015 at 20:23, William Stein <wst...@gmail.com> wrote:

<SNIP>

By the way, look at how coercion "works" in Magma:

$ magma
Magma V2.18-5     Thu Oct  1 2015 16:59:12 on compute3-us [Seed = 629019987]
Type ? for help.  Type <Ctrl>-D to quit.
> R<x> := PolynomialRing(IntegerRing());
> x + 1/2;

>> x + 1/2;
     ^
Runtime error in '+': Bad argument types
Argument types given: RngUPolElt[RngInt], FldRatElt

We are call this "complex coercion" in our Nemo discussions 

[...as opposed to simple coercion:

 R, x = PolynomialRing(QQ, "x")

 K, a = NumberField(x^3 + 3x + 1,"a")

 

 a + 1/2 # simple coercion since the result lives in K

]

It's definitely quite easy to add complex coercion in Nemo/Julia (via Julia generic catchall functions), but I'm resisting it quite obstinately for the time being.

One reason is that it easily leads to functions that are not type-consistent. You can quite easily write functions whose output type depends on the values, rather than the types of the inputs. This completely screws with type inference and Jit compilation, though Julia does allow it.

Since Nemo focuses on highly performant generics for the time being, I'm trying to avoid introducing complex coercions, at least until we have a very fast core. (Though naturally, mathematicians are keen to introduce this feature as soon as possible, since it is basically germane to any real mathematics.)

Bill.

[Bill Page]

On 1 October 2015 at 15:10, William Stein <wst...@gmail.com> wrote:
> On Thu, Oct 1, 2015 at 12:00 PM, Bill Page <bill...@newsynthesis.org> wrote:

>> ... Clearly the related? concept of

>> "element" is borrowed from category theory - maybe even topos theory?
>
> Yes, parents and elements are from Magma. To me they have nothing to
> do with category theory. Category theory is one level up, and is
> about abstracting away from thinking about parents and elements (and
> instead thinking about objects, morphisms, and functors). Just as
> Bill Hart said, the parent/element approach in magma is very useful,
> and inspired Sage and Nemo, but isn't category theory.
>

Thanks. I was thinking of elements as morphisms, as in that branch of
category theory.

[Bill Page]

In FriCAS

(1) -> x:Polynomial(Integer)
Type: Void
(2) -> x + 1/2

1
(2) x + -
2
Type: Polynomial(Fraction(Integer))

On 1 October 2015 at 15:28, 'Bill Hart' via sage-devel

[Francesco Biscani]

FWIW that's what Piranha does as well:

polynomial<integer,k_monomial> x{"x"};

 // This will print "1".

std::cout << std::is_same<decltype(x + 1/2_q),polynomial<rational,k_monomial>>::value << '\n';

[Bill Hart]

I once collected some amusing examples from Pari, Sage and Magma related to their different concepts of coercion. It can lead to all sorts of mathematical stupidity.

I concluded that trying to model maths this way is like trying to put a carpet down in a room with a wonky floor. You can locally get it quite flat, but once you get near a region that no one has flattened it's as crumpled as a Chinese Shar-pei.

After a little more research I discovered that maths papers weren't any better.

Bill.

[Simon King]

Hi Bill,

On 2015-10-01, Bill Page <bill...@newsynthesis.org> wrote:
>> I would expect that somebody who doesn't know category theory (the
>> mathematical area) would find the category framework in Sage very
>> confusing, just like somebody who doesn't know calculus might find the
>> symbolic functionality confusing.
>
> No, I find the Sage implementation of these ideas confusing, or at the
> very least overly complicated.

Indeed, when William states that someone who doesn't know category theory
mathematically might find Sage's category framework confusing, one can as
well state: Someone who has a profound knowledge about the mathematical
implications of category theory will be very confused by how Sage's
category framework works.

I am attending the annual meeting of a priority programme of German
science foundation, and there has also been a talk about CAP. It seems
to me that they really mean business with a constructive approach towards
category theory: When the user provides a construction algorithm for each
existence quantor appearing in the axioms (say, given a morphism one has
functions returning the kernel and its embedding into the domain, and
a function that returns, for each test object, the morphism whose
existence is granted by the universal property of the kernel), then CAP
will help you with things like connecting homomorphisms or spectral
sequences.

When I first encountered Sage's category framework, I expected to see something
similar to what we now have in CAP, but it has in fact a rather
different flavour and purpose.

Best regards,
Simon

[Simon King]

Hi William and Bill!

On 2015-10-01, William Stein <wst...@gmail.com> wrote:
>> Is there a reasonably short description of categories in Sage "for
>> category theorists"?

There is something about both parent-element scheme and category
framework in the thematic tutorial
http://doc.sagemath.org/html/en/thematic_tutorials/coercion_and_categories.html#coercion-and-categories

>> Do you consider the coercion model as part of or motivated by category
>> theory in Sage?
>
> Yes, very much so -- that's the part I worried about more. Though
> another motivation is for category theory is better code sharing
> (that's more of the part that Nicolas added).

Indeed, the underlying notions of the current coercion framework in Sage
are adopted from category theory:

- A coercion map is a morphism in an appropriate category containing both
domain and codomain.
- The identity morphism is a coercion.
- For each pair P,Q of objects there is at most one coercion morphism
from P to Q.
- The composition of a coercion morphism from P to Q with a coercion
morphism from Q to R is a (the!) coercion morphism from P to R.

Moreover, there is the notion of so-called "construction functors".
That's a functor F from category C to category D, such that for any
object P of C there is a coercion from P to F(P). For example, there is
a functor that maps each ring R to the polynomial ring R[x], and there
is a coercion from R to R[x].

William mentioned the example of adding a rational number to a
polynomial over the integers, resulting in a polynomial over the
rational numbers. What we see at work here is a combination of the
"fraction field" and the "polynomial ring" construction functors.

The above-mentioned tutorial provides examples for all that, and how to
implement it.

Best regards,
Simon

[Simon King]

Hi Bill,

On 2015-10-01, 'Bill Hart' via sage-devel <sage-...@googlegroups.com> wrote:
> One reason is that it easily leads to functions that are not
> type-consistent. You can quite easily write functions whose output type
> depends on the values, rather than the types of the inputs. This completely
> screws with type inference and Jit compilation, though Julia does allow it.

That's one of the reasons why people love the category framework in Sage
and why people hate the category framework in Sage:

sage: M1 = MatrixSpace(ZZ, 3)
sage: M2 = MatrixSpace(QQ, 3)
sage: M3 = MatrixSpace(QQ, 3, 4)
sage: type(M1) == type(M2)
False
sage: type(M2) == type(M3)
False
sage: M4 = MatrixSpace(Frac(QQ['x']), 3, 4)
sage: type(M4) == type(M3)
True
sage: type(M1).__base__ == type(M2).__base__ == type(M3).__base__ == type(M4).__base__
True

The reason for the above surprising behaviour: If a parent P uses the
category framework (as it is supposed to), then its Python class is
overridden by a dynamically created class that takes into account a
Python class that is assigned to the category in which P lives (yes,
Python allows that).

Here, we have:
sage: M1.category()
Category of infinite algebras over (euclidean domains and infinite
enumerated sets)
sage: M2.category()
Category of infinite algebras over quotient fields
sage: M3.category()
Category of infinite vector spaces over quotient fields
sage: M4.category()
Category of infinite vector spaces over quotient fields

And that explains the above findings.

Of course, all four matrix spaces above are instances of
sage.matrix.matrix_space.MatrixSpace

Best regards,
Simon

[Bill Page]

On 1 October 2015 at 17:38, Simon King <simon...@uni-jena.de> wrote:
> ...

> When I first encountered Sage's category framework, I expected to see
> something similar to what we now have in CAP, but it has in fact a rather
> different flavour and purpose.
>

Understood. I am not arguing against the way this was done in Sage
but I continue to wish for something both simpler and more ambitious.
:)

I am very interested in the use of adjunction in programming languages
and the definition of types by construction of universals. Perhaps CAP
is relevant? Can you provide a reference to a relevant paper?

Cheers,
Bill Page.

[Simon King]

Hi Bill,

On 2015-10-01, Bill Page <bill...@newsynthesis.org> wrote:

> On 1 October 2015 at 17:38, Simon King <simon...@uni-jena.de> wrote:
>> ...
>> When I first encountered Sage's category framework, I expected to see
>> something similar to what we now have in CAP, but it has in fact a rather
>> different flavour and purpose.
>

> I am very interested in the use of adjunction in programming languages
> and the definition of types by construction of universals. Perhaps CAP
> is relevant? Can you provide a reference to a relevant paper?

When I said "...what *we* now have in CAP", then "we" means "the
computer algebra community". I.e., I am not an author of CAP, and I
first learnt about it this week.

Best regards,
Simon

[Simon King]

PS:

On 2015-10-01, Bill Page <bill...@newsynthesis.org> wrote:

> I am very interested in the use of adjunction in programming languages
> and the definition of types by construction of universals. Perhaps CAP
> is relevant? Can you provide a reference to a relevant paper?

The talk on CAP here was presented by Sebastian Gutsche from
Kaiserslautern and Sebastian Posur from Aachen.

Best regards,
Simon

[Bill Page]

Thanks.

https://github.com/homalg-project/CAP_project

https://github.com/homalg-project/CAP_project/blob/master/CAPManual.pdf

[Bill Hart]

Bill, you may also like to see the HomAlg project:

http://homalg.math.rwth-aachen.de/

I know of this through some of its authors, Mohamed Barakat and Sebastian Gutsche, who both still list their affiliation on that website as Kaiserslautern.

That project is homological algebra. It is an innovative project that is obviously informed by category theory.

Bill.