Edit detail for SandBox Aldor Category Theory revision 12 of 12

This project is intended to implement the code and concepts presented by Saul Youssef in "Prospects for Category Theory in Aldor", 2004.

http://atlas.bu.edu/~youssef/papers/math/aldor/aldor.pdf

and the following slides:

http://atlas.bu.edu/~youssef/homepage/talks/categories/categories.html

The original code written by Saul is available here:

http://axiom-wiki.newsynthesis.org/public/london.tar.gz

The following links point to modified source code modules and tests of the Aldor programs in Axiom. The version of Aldor that is currently being used here is Rev: 16, Last Changed Date: 2007-11-09 from the Aldor source code repository. The version of Axiom is currently the FriCAS fork, Rev: 123, Last Changed Date: 2007-11-08.

• SandBox Aldor Category Theory Basics
• SandBox Aldor Category Theory Categories

This links and other information here will be updated as work continues. If you have some interest in category theory and in Aldor, I would encourage you to jump in here and help! :-) Comments on this work would also be greatly appreciated. On can submit comments just be filling out the comment form below.

Regards, Bill Page.

by Ralf Hemmecke Nov 05, 2007; 06:07pm

Saul Youssef wrote:

  http://atlas.bu.edu/~youssef/papers/math/aldor/aldor.pdf

  I still think that this is a good way to look for flaws in the
  language - implement category theory and see what goes wrong.

I quite like what you wrote. But I somehow fear that the compiler does not accept your code. Could you provide the compilable sources of this paper?

Furthermore, you do quite a lot of high-level constructions. To me it seems that they are OK to do category theory, but have you any comment how these constructions could be used to reduce the amount of programming work, i.e. code reuse?

Ralf

PS: Mistakes...

Page 5:

  Id(Obj:Category):Category == with
       id: (A:Obj) -> (A->A)
     default
       id(A: Obj):(A->A) == (a:A):A +-> a --rhx: I changed this line.

Page 10:

  homList(A:Categorify P,B:Categorify P):SingleInteger == add

should probably read:

  homList(A:Categorify P,B:Categorify P):List(A->B) ==

by Ralf Hemmecke Nov 08, 2007; 10:14am

First, thank you very much for your code. Under which license is it? Public domain, mBSD, GPL, ... ?

Unfortunately, the compiler has changed a bit:

  woodpecker:~/scratch/Youssef/london>aldor Basics.as
  woodpecker:~/scratch/Youssef/london>aldor Categories.as

  #1 (Error) There are 2 meanings for the operator `+'.
        Meaning 1: (Obj, Obj) -> Obj
        Meaning 2: (A: Obj, B: Obj) -> (
                 Obj with
               ...
  #2 (Error) There are 2 meanings for the operator `..'.
        Meaning 1: (Obj, Integer) -> Obj
        Meaning 2: (A: Obj, n: Integer) -> (
                 Obj with
           ...
  #3 (Error) There are 2 meanings for the operator `*'.
        Meaning 1: (Obj, Obj) -> Obj
        Meaning 2: (A: Obj, B: Obj) -> (
                 Obj with
               ...
  #4 (Error) There are 2 meanings for the operator `^'.
        Meaning 1: (Obj, Integer) -> Obj
        Meaning 2: (A: Obj, n: Integer) -> (
                 Obj with
           ...

In fact, I don't quite know how to resolve that problem. Actually, I wonder why I don't see any line numbers here.

I guess the commands "ao" and "ai" that I find in "compile" and "exercise" mean something like:

  alias ao=aldor -fao
  alias ai=aldor -G interp

Or did you use other scripts?

One of the things that encouraged me at the time was thinking about the simplest Aldor category in the mathematical sense: objects of the category are Aldor domains satisfying:

  Domain: Category == with  # no signatures (my favorite base category
  for a library)
</blockquote>

I wonder why you called it "Domain" and not something else? In some way you are right:

  A: Domain

then says that A is a domain. Sounds not too bad.

by Saul Youssef Nov 08, 2007; 12:30pm

First, thank you very much for your code. Under which license is it? Public domain, mBSD, GPL, ... ?

No problem. I offer it freely with no restrictions or claims.

Unfortunately, the compiler has changed a bit.

It might be useful for you just as a sample of odd code that should work but is structurally different from what you're used to.

#1 (Error) There are 2 meanings for the operator `+'. Meaning 1: (Obj, Obj) -> Obj Meaning 2: (A: Obj, B: Obj) -> ( Obj with ...

I haven't a clue about this, but that's why I included the old foam output in case it's a clue for you. This stuff was all compiled just before the London Ontario meeting in 2001.

I wonder why you called it "Domain" and not something else? In some way you are right:

  A: Domain

then says that A is a domain. Sounds not too bad.

I do think that this is nicer than "DomainCategory?", "SetCategory?" etc. In this style, you typically produce domains by applying domain constructors (i.e. "functors") and quotients rather than implementing them directly, so you might as well then keep the nice names for the categories.

by Bill Page-7 Nov 08, 2007; 01:16pm

I think the problem here is that the new version of the Aldor compiler needs a little more help just be reassured that you really are writing a function that returns a domain. The empty with {} clause seems to do the trick.

by Bill Page-7 Nov 21, 2007; 08:21pm

Saul,

I have been spending some time trying to compile your code for "computing with category theory" in the new open source release of Aldor and working on a version that I hope will work inside Axiom. But as Ralf noted it seems that either the compiler has changed in several subtle ways or perhaps your code as based on a somewhat different branch development of Aldor? In several places in your code you refer to "bugs in 1.1.12p6" and your hope that these will be solved so to enable to more complete implementation of your ideas. I am very curious what to what the version number 1.1.12p6 refers. From other statements you have made I am lead to believe that this relates to a version of Aldor that was available about 5 years ago. But the release number associated with the new open source release is just "officially" at release 1.1, now. Can you recall anything more specific about the version you used?

One reason that I would like to know the actual version of Aldor that you used and how it relates to the current version is because at least with respect to your code it seems that the new version of the compiler may have regressed in some very interesting areas of application (to me at least). This might suggest that we need a more complete set of regression tests for this style of programming or perhaps it relates to some specific design concompromizes in the language that have come to light since you did you work on this subject.

Also of course I would very much like to have an operational version of code with which to play and perhaps I would be able to install an older version of Aldor that would allow me to do that. This would certainly help in trying modify the code in such a manner that it will work on the newer version of Aldor and in the Axiom environment.

by Saul Youssef Nov 21, 2007; 10:36pm

Aldor version:

It's something that I got directly from Stephen Watt. I think that it was the main branch at the time, not a side development branch of any sort.

I'm not sure, but I think that this might be a release that Stephen distributed at the 2001 workshop.

by Ralf Hemmecke Nov 23, 2007; 11:00am

I think, I don't like your suggestion. I'd rather change it into:

  define Product(Obj:Category):Category == with {
         ...
  --        *:(Obj,Obj)->Obj;
     default {
         local mult(A:Obj, B:Obj):Obj == {
                 (
                     AB:Obj,
                     pa:AB->A,
                     pb:AB->B,
                     product:(X:Obj)->(X->A,X->B)->(X->AB)
                 ) == Product(A,B);
                 AB add;
         }
         *: (Obj,Obj)->Obj == mult;
     }
  }

The "default" is like defining an anonymous "add" body which exports anything on the left of == that is not declared local. So:

   *: (Obj,Obj)->Obj

will get exported by Product(Obj) even if you put a "--" as I did above.

by Bill Page-7 Nov 23, 2007; 12:04pm

Thanks, Ralf. I like your version better than mine. It makes more sense than the apparently redundant syntactic change I proposed ... although I wonder why we should define a local function rather than just write it inline. Would you agree however that that fact that Saul's original variant does not compile should be considered a regression bug in the Aldor compiler?

Regards, Bill Page.

by Ralf Hemmecke Nov 23, 2007; 12:40pm

Yes and no.

Suppose you want to declare:

  ---BEGIN aaa.as
  #include "aldor"
  define Cat: Category == with {
       foo: String -> Integer;
       foo: (s: String) -> Integer;
  }
  ---END aaa.as

The types of both foos are different. The question now is, would you like Cat to export 2 or only 1 function?

Now there is a very special case...

Would you like X and Y:

  X: Record(x: A);
  Y: Record(y: A);

be of the same type?

So I cannot really say yes or no to your question and would rather be happy to hear more information from the people who changed the compiler behaviour.

What is the background? And (more importantly) what is the semantics of "Cat" according to the language definition. I cannot say whether it exports one or two functions.

Ralf

by Saul Youssef Nov 23, 2007; 01:05pm

Hi Bill, Ralf,

To put things in perspective, I tried two alternative definitions of Product and coProduct besides the ones in Categories.as. One is as the right adjoint of the diagonal functor (Ideal.as) and the other is as a special case of general limits and colimits (Limits.as). The last two seemed like that should work in the language, but didn't due to compiler problems. The one in Categories.as got used only because it's the only one of the three that worked at the time.