[Axiom-math] Re: [Aldor-l] Type equivalence of domains in Axiom and Aldor

[Saul Youssef]

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.

- Saul

On 11/23/07, Ralf Hemmecke <address@hidden> wrote:
> Hello Bill,
>
> 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.
>
> Ralf
>
>
> On 11/08/2007 07:51 PM, Bill Page wrote:
> > Ralf,
> >
> > Here is another version that is slightly more friendly to the #pile
> > syntax (-: no {}  required :-). I presume that the compiler generates
> > the same code...
> >
> > --- Categories.as_orig  2007-11-08 10:09:11.000000000 -0800
> > +++ Categories.as       2007-11-08 10:45:51.000000000 -0800
> > @@ -66,3 +66,3 @@
> >      Product: (A1:Obj,B1:Obj,  A2:Obj,B2:Obj) ->
> > (AB1:Obj,AB2:Obj,(A1->A2,B1->B2)->(AB1->AB2))
> > -    *:(Obj,Obj)->Obj
> > +    *:(Obj,Obj)-> with Obj
> >      default
> > @@ -73,3 +73,3 @@
> >             (ab1,ab2,*)
> > -        (A:Obj)*(B:Obj):Obj ==
> > +        (A:Obj)*(B:Obj): with Obj ==
> >              
> > (AB:Obj,pa:AB->A,pb:AB->B,product:(X:Obj)->(X->A,X->B)->(X->AB))
> > == Product(A,B)
> > @@ -83,3 +83,3 @@
> >      CoProduct: (A1:Obj,B1:Obj, A2:Obj,B2:Obj) ->
> > (AB1:Obj,AB2:Obj,(A2->A1,B2->B1)->(AB2->AB1))
> > -    +:(Obj,Obj)->Obj
> > +    +:(Obj,Obj)-> with Obj
> >      default
> > @@ -90,3 +90,3 @@
> >             (ab1,ab2,+)
> > -        (A:Obj)+(B:Obj):Obj ==
> > +        (A:Obj)+(B:Obj): with Obj ==
> >              
> > (AB:Obj,ia:A->AB,ib:B->AB,product:(X:Obj)->(A->X,B->X)->(AB->X))
> > == CoProduct(A,B)
> > @@ -99,5 +99,5 @@
> >      Product:(A:Obj,n:Integer)   ->
> > (Prod:Obj,Integer->(Prod->A),(X:Obj)->(Tuple (X->A))->(X->Prod))
> > -    ^:(Obj,Integer) -> Obj
> > +    ^:(Obj,Integer) -> with Obj
> >      default
> > -        (A:Obj)^(n:Integer):Obj ==
> > +        (A:Obj)^(n:Integer): with Obj ==
> >             (Prod:Obj,project:Integer->(Prod->A),product:(X:Obj)->(Tuple
> > (X->A))->(X->Prod)) == Product(A,n)
> > @@ -110,5 +110,5 @@
> >      CoProduct:(A:Obj,n:Integer) -> (
> > Sum:Obj,Integer->(A->Sum),(X:Obj)->(Tuple (A->X))->(Sum->X))
> > -    ..:(Obj,Integer) -> Obj
> > +    ..:(Obj,Integer) -> with Obj
> >      default
> > -        (A:Obj)..(n:Integer):Obj ==
> > +        (A:Obj)..(n:Integer): with Obj ==
> >             (Sum:Obj,insert:Integer->(A->Sum),sum:(X:Obj)->(Tuple
> > (A->X))->(Sum->X)) == CoProduct(A,n)
> > address@hidden:~/aldor-src/aldor/install/aldor#
> >
> > ----
> >
> > Regards,
> > Bill Page.
> >
> > On 11/8/07, Bill Page <address@hidden> wrote:
> >> Ralf,
> >>
> >> 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.
> >>
> >> Here is a patch to 'Categories.as' that allows it to compile... but I
> >> have not yet compiled the rest so I am not 100% sure that the end
> >> result will be ok. (Also attached as a file.):
> >>
>
>
>