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

[Bill Page]

William,

I think these are great examples with which to examine
some fundamental ideas in Axiom!

On Thursday, January 13, 2005 2:56 AM you wrote:
>...

> --%PointedPrimeField
> )abbrev domain PPF PointedPrimeField
> PointedPrimeField(n:PositiveInteger):Cat==Dog where
>   Cat == FiniteFieldCategory with
>     foo:PositiveInteger->PrimeField(n)
>   Dog == PrimeField(n) add
>     foo(k)==k::Integer::PrimeField(n)
>
> After compiling, define in the interpreter
>
> g(n,k)==foo(k)$PPF(n)
>
> Compiling g is still a problem in Axiom due to signature
> limitation. At least this way, inlininga complicated
> function is almost like a function call.
>

>From a mathematical point of view I think this "signature
limitation" in Axiom is natural and that Aldor goes too
far in allowing a construction like

  g(n:Integer,k:Integer):PrimeField(n)

when defining functions. The reason is that I do not see
how it is possible to interpret PrimeField(n) as a domain
in the normal ("categorical") sense, in this context where
the value of n is not known.

Of course from a programming point of view we do know how
to interpret the Aldor construction and apparently Aldor
knows how to compile it. But I do not think that this
necessarily makes it desirable in a language that is
primarily intended to be efficient and accurate in the
definition of mathematical concepts.

> 
> The idea is: Since in creating domains, we are in effect 
> creating a function (the domain constructor PPF is a
> function of sort, or functor) and the compiler can
> take dependent types in its signature, structurally:
>   PPF(n:PositiveInteger)==PrimeField(n) with foo so it
> should be able to compile something like g by lifting 
> it to the package level.

Yes! I think you are exactly right. And it is politically
correct from the Axiom perspective to refer to this
construction as a "functor". I think it is a *good thing*
that Axiom's syntax encourages one to make this distinction.

> 
> So here is another way using package.
> 
> --%Foo
> )abbrev package FOO Foo
> Foo(n:PositiveInteger, k:PositiveInteger):T==C where
>   T == with
>        point:()->PrimeField(n)
>   C == add
>        point()==k::Integer::PrimeField(n)
> 
> After compiling, we can use
> 
>   point()$Foo(n,k)
> 
> in any computation in compiler code (and in interpreter). 
> Still can't call this g(n,k) unless you use a macro
> expansion:
> 
> g(n,k)==>point()$Foo(n,k)
> 

The use of a macro is ok because no signature is implied.

I think I prefer your first construction to the latter
because it is nice to think conceptually of foo(k) as
belonging to each of the PPF(n) domains, i.e. for each n.

Thinking of Foo(n,k) as a collection of "domains"
parameterized by n and k; and point() as belonging to
each such domain seems a little unnatural. Well I guess,
because Foo is a package ... Packages are for convenient
programming, not mathematical relationships.

I suppose what I am trying to say is that in the design
of the Axiom language we should be aware not only of
programming issues but also conceptual mathematical issues.

Regards,
Bill Page.