Re: [Axiom-developer] Axiom domains and Aldor return types

[William Sit]

Hi Bill:

Bill Page wrote:

> Just to be clear on my criticism: I am *not* against the use
> of dependent types as such. I just think that we should not
> call something that has dependent types a *function*. I think
> the Aldor notation risks confusion on a very fundamental
> mathematical issue. Axiom's spad language design make it clear
> that what Martin wants is really a *functor* (as you explained
> very clearly in your previous message - thank you!) Functors
> have a description (I dare not call it a "signature") which
> is more complex than a function. I think it is natural that
> Axiom's notation makes a clear distinction.

I think something like F(a:A)==F(a):B(a) should simply be called a program or
routine! It is neither a function nor a functor in the strict mathematical
sense.

> Is there a way that this "Aldor function" can be written
> in Aldor that syntactically respects the same distinction?
> If so, then perhaps we should just consider the way Aldor
> allows this to be written as a kind of abbreviation that
> happens to look like the notation for a function.

I think Aldor treats the two levels equally, that is, domain constructors and
"function" are the treated the same. Axiom does not and restricts "function" to
a real mathematical function while leaving domain (or even category and package)
constructors a bit more general by allowing dependent signatures. This allowed
dependence is even more general than F(a:A)==F(a):B(a), for example, one can
have F(a:A,b:B(a),c:C(a,b))==F(a,b,c):D(a,b,c). Such dependence is not allowed
for functions in Axiom but allowed in Aldor. In other words, the source does not
have to be "rectangular" but can be any "area" (or "solid") with bounding
"curves" ("surfaces"). Metaphorically, Aldor allows integration over any solid,
Axiom only over a cuboid. If you think about this calculus analogy, you can see
that Aldor is a much more powerful language. 

> BTW, chapters 11 Packages, 12 Categories and 13 Domains of the
> Axiom book are very useful but I find the orientation rather
> confusing - perhaps it is just the "age" of the terminology
> that is used in these chapters that makes reading a little hard.
> I think it would be great if these could be re-written in a
> more modern "categorical" manner similar to the way you wrote
> your previous message. Are there any papers that you could
> reference that attempt to do this? Is there some corresponding
> part of the Aldor documentation that would be useful for me
> to re-read?

Well, I tried to look up something from the web for my email on functors, and I
got a nice one for you:

http://math.ucr.edu/home/baez/categories.html

Actually, I was attempting to explain why something like Integer is a category
and I remembered that category theorist think of a group as a category but
forgot how. The above article explains that.  But applying the same to Axiom
does not work! Try it.

William