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

[William Sit]

Hi Bill and Martin:


Bill Page wrote:
> 
> William,
> 
> I think these are great examples with which to examine
> some fundamental ideas in Axiom!

You are absolutely correct that we need to analyse these ideas. In trying to
explain below these fundamental ideas, I discover how vague my "understanding"
was (and probably still is). You raised many good questions. This will be a
rather long analysis.

> 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, inlining a 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.

Martin Rubey wrote:

\ I agree that the limitation looks natural. However, if you 
\ look closer at Aldors design, it couldn't be clearer.

I'll argue that the limitation is not natural.

If all objects are first class (whatever that means), then there is not much
difference (syntactically speaking, except on a different level) between the two
*signatures*:

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

and

   DMP(v:List Symbol, R: Ring):_
     PolynomialCategory(R,_
       Direct Product(#(v),NonNegativeInteger),_
       OrderedVariableList(v))

The returned type in each case depends on the parameter(s). In each case, the
target category (we'll see how later) depends on input parameters (not just the
constructed object): for DMP, the target category depends on R, v and for g, it
depends on n. So it is entirely logical to allow the signature of g in Aldor.
But these do not spell out the codomain (target) in the sense of a mathematical
function. Both would present a problem. On first glance, it seems the
*signature* of PPF is

   PPF(n:PositiveInteger):FiniteFieldCategory

and its codomain does not depend on parameters and so as a mathematical
function,
 
   PPF: PositiveInteger -> FiniteFieldCategory

is ok. But actually, the correct *signature* of PPF is

   PPF(n:PositiveInteger):FiniteFieldCategory with_
     foo: PositiveInteger -> PrimeField(n)

so, it too, has a problem. All the functions (exports in Axiom jargon) in
PolynomialCategory are simply hidden in its category definition. We did not
create one for FiniteFieldCategory with foo. If we did, we would come up with
the same dependency.

So in what sense are domain constructors and functions functors? 

A functor must describe two things: how to map the objects, and how to map the
morphisms, of the source category. So the first question is: what are the
objects and morphisms in Axiom "categories"?

Take the source of DMP (DMP is a typical domain constructor). It is a direct
product of an Axiom domain: List Symbol, and an Axiom category: Ring.  DMP maps
an element (v,R) in this direct product to another Axiom domain which belongs to
the Axiom category POLYCAT (used here to stand for the longer, parametrized,
category PolynomialCategory).  So, is (v,R) an object of some category, or is it
a morphism? It would seem that it should be an object and indeed I believe it
is. The source of DMP is a category whose objects are pairs (v,R) and whose
morphisms are pairs of maps (f,h), where f:v ->v' is a set map, and h: R -> R' a
ring homorphism. There is a (more general) package called
PolynomialCategoryLifting, with a function named map that, when applied to the
DMP situation, would take a morphism

    (f,g): (v,R) -> (v', R') 

and "lift" this to a morphism of DMP(v,R) -> DMP(v',R'), thus providing the
mapping of DMP on morphisms.

Now what about the function g above? How is it a functor?

The source of g is the direct product 

     PositiveInteger x PositiveInteger. 

If its objects are pairs (n,k) of positive integers, then what are the morphisms
between them? It would seem that there is exactly one obvious "morphism" between
two pairs. The map g takes (n,k) to an element in PrimeField(n). So we must
treat PrimeField(n) itself as a category. Its objects would be numbers modulo n
(elements of the prime field) and again, there is only one obvious morphism
between two objects. But notice that this is only on the set level. The
algebraic structure of PrimeField(n) is totally neglected when we viewed it as a
category this way. Given this setting, g((n,k)) = k mod n, and g((n,k)->(n',k'))
= (k mod n)->(k' mod n').  

But are these really functors in the mathematical sense? Not yet. The problem is
in the target category. In mathematics, a functor has the form F: A -> B or
F(a:A)==F(a):B, where both A and B are categories, and B does not depend on any
particular object of A. A functor consists of a bunch of mathematical set
mappings (objects of A to objects of B, Hom(X,Y) to 
Hom(F(X),F(Y))). In Axiom's functors, B may depend (and often does) on the
parameters from A. So it has the form 
F(a:A)==F(a):B(a).  You may say this generalizes the usual notion of a functor.
But that neglects the morphisms! In axiom, F seldom explicitly says what
F(a->a') is, because, it would have to be a morphism in a category between F(a)
and 
F(a'). But F(a) and F(a') belong to two different categories 
B(a) and B(a'), respectively, and you really cannot talk about morphisms between
objects in different categories except in very special cases when both
categories B(a) and B(a') are subcategories of a category C.

So back to my previous analysis on DMP. There, I actually made a mistake by
being careless (I deliberately left it the way it was). I should have used
POLYCAT(v,R) (not in correct Axiom syntax, but used to stand for the longer,
parametrized, category PolynomialCategory based on v and R given in the
*signature* of DMP above) instead of POLYCAT. Then I would have noticed that we
need to put the R-algebra
DMP(v,R) and the R'-algebra DMP(v',R') into one category.
This can be done if all R:Ring are of the same characteristic, say zero. We can
then consider these as Z-algebras (Z = Ring of integers) and the map
DMP(v,R)->DMP(v',R') would be a Z-algebra morphism.  But DMP(v,R) has more
structure, for example, it is an R-algebra, and in fact the lift map is an
R-algebra homomorphism too (via the map h:R->R', R' becomes an 
R-algebra). So, just as in the case of the function g, where we forget about
some structure of PrimeField(n), we must forget about the some algebraic
structures of DMP(v,R). 
 
Conclusion, if my analysis is correct: In Axiom, domain constructors are
functors into the category Set, and perhaps subcategories in some cases. Viewed
this way, there is no dependence on input parameters in the target category.
Computationally, we of course want to keep track of which subcategory the
domains are and it would be nice to allow that in the signature, not just of
domain constructors, but for functions.

To paraphrase a famous quote: There is no such thing as a simple explanation.

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

See above.

Martin Rubey wrote:

\ Well, if it would be only encouragement... However, there 
\ is no way to do it differently! I'm sure it is not too
\ difficult to come up with an example where the solution 
\ above won't work.

In terms of the function computations, I think both the domain version and the
package version would suffice -- not as convenient as it would be, but these
will work. The only situation I can think of that will be a problem is where the
signature of the function is actually needed (meaning, written down). An example
would indeed be interesting.

\ There is another, different point I'd like to make:
\ 
\ Aldor has been designed to be "cleaner" than Axioms internal
\ language. Not that much has changed, it seems that they were
\ very careful, and it's quite certain that these were very 
\ clever people. I think it would be wiser to adopt Aldor
\ (which won't break much) rather than to try to extend Axioms
\ own language and let the two languages diverge. I simply
\ don't see the point.

The problem is that Aldor has implemented only a small fraction of the algebra
code in Axiom. Didn't someone just mentioned that PositiveInteger is not in
Aldor? (May be that is good, trust the programmers and get rid of a lot of
needless coercions).  

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

The above macro is not that good, because you cannot replace n or k by
expressions.

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

Isn't it nice to have two ways? :-)
But I think the package version mirrors the original function g(n,k) better
because it use the same syntax, except that g is replaced by point()$Foo, and
one can replace n and k by expressions. I was avoiding the macro

   g ==> point()$Foo

and used

   bar ==> point()$Foo

to avoid replacing all "g" in a program!

Bill Page wrote:
> See
> 
> http://page.axiom-developer.org/zope/mathaction/DynamicFunctionDomains#msg20
> address@hidden
> 
> but notice that your use of the macro near the end produces
> and error.
> 
> > bar ==>point()$Foo
> >
> >                  Type: Void
> >bar(4,7)
> >   Although Foo is the name of a constructor, a full type 
> >must be specified in the context you have used it. Issue 
> >)show Foo for more information.
> 
> It appears to be trying to evaluate bar before concatonation
> with `(4,7)'.

You are right. The same happens with the compiler. 

   bar(4,7)

would be parsed as

   ((|elt| |Foo| |point|)) |n| |k|

but should be

   ((|elt| (|Foo| |n| |k|) |point|)) 
  
Anyway, there is little saving to use a macro except that it looks more like the
original function. So the following works:

)abbrev package BARTEST Bartest
Bartest: T==C where
   T == with
        barrun: () -> Void
   C == add
        import FOO
        barrun() == 
          for k in 4..5 repeat
            for n in [1,2,4,6]::List PositiveInteger repeat
              print(point()$Foo(n+1,k)::OutputForm$PrintPackage

barrun()

The point is, it is compilable.

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

Agreed with no reservations.


William