[Aldor-l] [sage-devel] Re: [sage-combinat-devel] Categories for the working programmer

[Bill Page]

On Tue, Nov 11, 2008 at 4:42 AM, Ralf Hemmecke wrote:
>
>> Finally, I should note that I do not agree with Ralf's views (quoting
>>  Doye's article on Aldor) on the importance of universal algebra
>> notions to categories in Axiom.
>
> Maybe it belongs somewhere else,
>

I agree that this discussion probably doesn't belong on sage-devel so
I reply here on the aldor and fricas-devel lists.

> but how would you explain to someone who is new to Aldor/panAxiom,
> what the concept of "category" in the Aldor/panAxiom language is?
> That is a language concept.

Like Stephen, I would explain that a category in Aldor/panAxiom is
just a named collection of domains - nothing more, nothing less. When
we write:

   Foo1():Bar == add ...
   Foo2():Bar == add ...

we mean that the domains Foo1, Foo2, ...  are members of the category Bar.

You might ask: "What about the exports?".

I would explain: Associating exports with categories is just a
convenience. We require that these exports be implemented by all
domains that belong to such a category. But nothing in Alor/panAxiom
would change if we removed all of the exports from the category and
specified them explicitly in each domain that belongs to that
category.

For example, consider the category

  Bar():Category == with
    f:X -> Y

Now we must define f in any domain that belongs to Bar:

  Foo():Bar == add
      f(x:X):Y == ...

But if no exports were associated with Bar(), we could still write:

  Foo():Bar with
      f:X->Y
    == add
      f(x:X):Y == ...

and everything would be the same. Note that the declaration Foo is a
member of Bar must remain! Or do you think I am missing some other
important feature of the language?

Default functions in categories are a similar "convenience" that
together with the use of the symbol % and parameters allows a form of
generic programming. E.g.

  Bar(X:IntegerNumberSystem):Category == with
      f:X -> %
    add
      f(x:X):% == ...

Then just declaring

  Foo():Bar(Integer) == add

defines a domain that exports f.

> Then comes the question whether an Axiom category is in some way
> related to some known mathematical concept.

Categories, as collections of domains are naturally organized into a
sub-category lattice. The relationship between categories is
inclusion.

   Bar():Category == Join(Bar1, Bar2)

>From the point of view of lattice theory "Join" is poorly named
(should really be Meet) but Join makes sense when one is focused on
the list of exports.

Categories that take parameters are functions (functors?) that denote
collections of domains.

> For me order-sorted algebras match quite well

To be an order-sorted algebra (for example as promoted by Joseph
Goguen: http://www-cse.ucsd.edu/~goguen ), categories in
Aldor/panAxiom would have to implement a great deal more than what is
done at present. We should expect to see universal algebra-like
operations like quotient, image, product and term algebras, etc.
Aldor/panAxiom has none of these. I might agree that the concept of
order-sorted algebras could serve as a kind of "design principle" to
suggest how to actually use categories in Aldor/panAxiom but in the
end, the axioms and how we use categories in Aldor/panAxiom are just
conventions.

> while (mathematical) category doesn't (even if that might
> have been the original motivation for the name in Axiom).

I am not convinced that the original Axiom developers ever intended
that categories in Axiom would have anything to do with categories in
mathematics. On the other hand as you know Saul Youssef has
demonstrated that it is also possible to use category theory in Aldor
as a similar sort of "design principle" for library code.

> ...

Regards,
Bill Page.