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

[Saul Youssef]

Hi Ralf,

>
> I quite like what you wrote.

Thanks.

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

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.

>
> 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?

Category theory is famous for seeming to be about nothing, but still
being one of the most important ideas from 20th century math anyway.
Possibly the best thing is to look at Groups.as to get a flavor of
something concrete happening.   This implements the category of groups
(in the math sense) and is described a little bit in this talk as a
more concrete example

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

There's a whole field of "applications of category theory to computer
science" with ten years of conferences at least (which I know next to
nothing about), but still, as far as I know, there is no language
where one can conveniently create and manipulate categories, objects,
morphisms, adjoints, etc.  Having this, I think, could suddenly make a
huge difference and open up many powerful applications.

     From the computing, re-use of code and correctness points of
view, for example, I think that the situation is quite promising.
For example, in category theory, groups come together with group
homorphisms having the property f(g*h) = f(g)*f(h).  The usual problem
is that it is next to impossible for the compiler to check that a
given function has this property.  On the other hand if f is produced
by a "functor" (e.g. the free construction domain constructor in the
code above), f is guaranteed to have the property.  The same holds for
all categories.  For code re-use, you not only can have common code
for all groups, say, you can have common code for all categories or
for categories with additional properties (e.g. abelian categories).
"Adjoint", in the paper, is a not completely trivial example of this.
It's defaults, for example, have the code which maps morphisms from
one category to morphisms in another.

    I suspect that could help you alot to be aware of this stuff if
you're not already (sorry if I'm saying stuff that's obvious for you).
 For instance, the issue came up in this thread: what should be the
definition of equivalent domains and how should that be computed?  In
category theory, if A and B are domains of the same category, they are
isomorphic exactly when there exists morphisms f:A->B and g:B->A with
g o f = 1, f o g = 1.  That's the right answer from the mathematical
point of view.  If Aldor produces a different answer, it's going to
cause suffering down the road because it will be close to, but not
quite what one wants mathematically.

     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)

and morphisms are Aldor functions.  Even though Domain has no
signatures, the statement that it is a category in the mathematical
sense is true but not trivial - one has to *assume* that composition
of Aldor functions is associative.  Also, this category already has
direct products and direct sums (essentially Record and Union).  Given
the category Domain, you could introduce "Set" with "=" and produce
Set domains by applying a free construction domain constructor to
Domains just like in the group case.

Best regards,

   - Saul

>
> 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) ==
>
>
>

london.tar.gz
Description: GNU Zip compressed data