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

[Bill Page-7]

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.

_______________________________________________
Aldor-l mailing list
Aldor-l@...
http://aldor.org/mailman/listinfo/aldor-l_aldor.org

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

_______________________________________________
Aldor-l mailing list
Aldor-l@...
http://aldor.org/mailman/listinfo/aldor-l_aldor.org