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

[Ralf Hemmecke]

On 11/12/2008 05:06 AM, Bill Page wrote:
> 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?

With that one can, of course, say that Foo is a member of Bar.

But if I consider the last definition and I only have the knowledge that 
the type of Foo is Bar, then I cannot call f$Foo since Bar doesn't claim 
that there is such a function export.

With your first two definitions f$Foo is know to exist.

> Default functions in categories are a similar "convenience"

I agree.

> 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):% == ...

Why do you think that % is important here? (But your sentence doesn't 
make quite clear whether you want to go into this discussion.)

> 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.

But if you leave out the exports of (Axiom-)categories, you can never 
speak of the category of rings or such things.

> 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

Good. I meant nothing more.

> but in the
> end, the axioms and how we use categories in Aldor/panAxiom are just
> conventions.

That is really a pitty. There is a real need that one can specify axioms 
with panAxiom/Aldor that are understood by the compiler. I'd like to 
give input/output specifications in a more formal manner than just in 
documentation.

> 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.

Unfortunately his code is largely undocumented. And I still have no real 
impression of how useful it is computationall. The seem to be more 
(aldor-)category definitions than actual domains. So I still don't say 
much to Saul's code except that I am quite impressed of what he did.