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

[Ralf Hemmecke]

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