[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Axiom-math] Re: [Aldor-l] Type equivalence of domains in Axiom and Aldo
From: |
Bill Page |
Subject: |
[Axiom-math] Re: [Aldor-l] Type equivalence of domains in Axiom and Aldor |
Date: |
Thu, 8 Nov 2007 13:16:56 -0500 |
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.):
address@hidden:~/aldor-src/aldor/install/aldor# aldor Categories.as
address@hidden:~/aldor-src/aldor/install/aldor# diff -au Categoris.as_orig
Categories.as
diff: Categoris.as_orig: No such file or directory
address@hidden:~/aldor-src/aldor/install/aldor# diff -au Categories.as_orig
Categories.as
--- Categories.as_orig 2007-11-08 10:09:11.000000000 -0800
+++ Categories.as 2007-11-08 10:11:54.000000000 -0800
@@ -64,14 +64,14 @@
define Product(Obj:Category):Category == with
Product: (A:Obj,B:Obj) -> ( AB:Obj, AB->A, AB->B,
(X:Obj)->(X->A,X->B)->(X->AB) )
Product: (A1:Obj,B1:Obj, A2:Obj,B2:Obj) ->
(AB1:Obj,AB2:Obj,(A1->A2,B1->B2)->(AB1->AB2))
- *:(Obj,Obj)->Obj
+ *:(Obj,Obj)->Obj with {}
default
Product(A1:Obj,B1:Obj,A2:Obj,B2:Obj):(AB1:Obj,AB2:Obj,(A1->A2,B1->B2)->(AB1->AB2))
==
(ab1:Obj,pa1:ab1->A1,pb1:ab1->B1, product1: (X:Obj) ->
(X->A1,X->B1) -> (X->ab1)) == Product(A1,B1)
(ab2:Obj,pa2:ab2->A2,pb2:ab2->B2, product2: (X:Obj) ->
(X->A2,X->B2) -> (X->ab2)) == Product(A2,B2)
(f:A1->A2)*(g:B1->B2):(ab1->ab2) == product2 ( ab1 )(
(x:ab1):A2 +-> f pa1 x, (x:ab1):B2 +-> g pb1 x )
(ab1,ab2,*)
- (A:Obj)*(B:Obj):Obj ==
+ (A:Obj)*(B:Obj):Obj with {} ==
(AB:Obj,pa:AB->A,pb:AB->B,product:(X:Obj)->(X->A,X->B)->(X->AB))
== Product(A,B)
AB add
@@ -81,14 +81,14 @@
define CoProduct(Obj:Category):Category == with
CoProduct: (A:Obj,B:Obj) -> ( AB:Obj, A->AB, B->AB,
(X:Obj)->(A->X,B->X)->(AB->X) )
CoProduct: (A1:Obj,B1:Obj, A2:Obj,B2:Obj) ->
(AB1:Obj,AB2:Obj,(A2->A1,B2->B1)->(AB2->AB1))
- +:(Obj,Obj)->Obj
+ +:(Obj,Obj)->Obj with {}
default
CoProduct(A1:Obj,B1:Obj,A2:Obj,B2:Obj):(AB1:Obj,AB2:Obj,(A2->A1,B2->B1)->(AB2->AB1))
==
(ab1:Obj,ia1:A1->ab1,ib1:B1->ab1, sum1: (X:Obj) ->
(A1->X,B1->X) -> (ab1->X)) == CoProduct(A1,B1)
(ab2:Obj,ia2:A2->ab2,ib2:B2->ab2, sum2: (X:Obj) ->
(A2->X,B2->X) -> (ab2->X)) == CoProduct(A2,B2)
(f:A2->A1)+(g:B2->B1):(ab2->ab1) == sum2 ( ab1 ) (
(x:A2):ab1 +-> ia1 f x, (x:B2):ab1 +-> ib1 g x )
(ab1,ab2,+)
- (A:Obj)+(B:Obj):Obj ==
+ (A:Obj)+(B:Obj):Obj with {} ==
(AB:Obj,ia:A->AB,ib:B->AB,product:(X:Obj)->(A->X,B->X)->(AB->X))
== CoProduct(A,B)
AB add
@@ -97,9 +97,9 @@
+++
define MultiProduct(Obj:Category):Category == with
Product:(A:Obj,n:Integer) ->
(Prod:Obj,Integer->(Prod->A),(X:Obj)->(Tuple (X->A))->(X->Prod))
- ^:(Obj,Integer) -> Obj
+ ^:(Obj,Integer) -> Obj with {}
default
- (A:Obj)^(n:Integer):Obj ==
+ (A:Obj)^(n:Integer):Obj with {} ==
(Prod:Obj,project:Integer->(Prod->A),product:(X:Obj)->(Tuple
(X->A))->(X->Prod)) == Product(A,n)
Prod add
@@ -108,9 +108,9 @@
+++
define CoMultiProduct(Obj:Category):Category == with
CoProduct:(A:Obj,n:Integer) -> (
Sum:Obj,Integer->(A->Sum),(X:Obj)->(Tuple (A->X))->(Sum->X))
- ..:(Obj,Integer) -> Obj
+ ..:(Obj,Integer) -> Obj with {}
default
- (A:Obj)..(n:Integer):Obj ==
+ (A:Obj)..(n:Integer):Obj with {} ==
(Sum:Obj,insert:Integer->(A->Sum),sum:(X:Obj)->(Tuple
(A->X))->(Sum->X)) == CoProduct(A,n)
Sum add
address@hidden:~/aldor-src/aldor/install/aldor#
--------
Regards,
Bill Page.
On 11/8/07, Ralf Hemmecke <address@hidden> wrote:
> Thank you Saul,
>
> 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'm attaching my code from the time (~3k lines) which includes the
> > bits in the paper. It all actually at least used to compile and work
> > in 2001.
>
> 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)
>
> 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.
>
> Ralf
>
> _______________________________________________
> Aldor-l mailing list
> address@hidden
> http://aldor.org/mailman/listinfo/aldor-l_aldor.org
>
Categories.patch
Description: Binary data
- [Axiom-math] Re: [Aldor-l] Type equivalence of domains in Axiom and Aldor, Ralf Hemmecke, 2007/11/06
- [Axiom-math] Re: [Aldor-l] Type equivalence of domains in Axiom and Aldor, Saul Youssef, 2007/11/07
- [Axiom-math] Re: [Aldor-l] Type equivalence of domains in Axiom and Aldor,
Bill Page <=
- [Axiom-math] Re: [Aldor-l] Type equivalence of domains in Axiom and Aldor, Bill Page, 2007/11/08
- [Axiom-math] Re: [Aldor-l] Type equivalence of domains in Axiom and Aldor, Ralf Hemmecke, 2007/11/23
- [Axiom-math] Re: [fricas-devel] Re: [Aldor-l] Type equivalence of domains in Axiom and Aldor, Bill Page, 2007/11/23
- [Axiom-math] Re: [open-axiom-devel] [fricas-devel] Re: [Aldor-l] Type equivalence of domains in Axiom and Aldor, Ralf Hemmecke, 2007/11/23
- [Axiom-math] Re: [Aldor-l] Type equivalence of domains in Axiom and Aldor, Saul Youssef, 2007/11/23