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

[Ralf Hemmecke]

Dear Saul,

>       Your questions have definite answers in category theory and
> since Aldor is *almost* doing category theory, it's tempting to think
> that the categorical answers to your questions are really what should
> naturally fit into the language.  I wrote up something trying this out
> for the 2001 workshop
> 
> 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) ==