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

[Bill Page]

William et al.

On Friday, January 14, 2005 11:51 AM you wrote:
> 
> Stephen Wilson wrote:
> 
> > Lifting everything to the package level is an example of 
> > how one will rapidly diverge from the math. For example,
> > what if instead of a functor
> > `PPF(n:PositiveInteger)==PrimeField(n) with ...'
> > we want something more general, like, say, given any
> > commutative ring R and a maximal ideal M in R we want the
> > quotient field R/M.
> > ...
> > But with dependent typing one can achieve this generality,
> > since the required function is a categorical export, which
> > each individual domain satisfies in its own way. It becomes
> > possible to write extraordinarily generic algorithms given
> > such a language facility.
> 
> I am not following your example. RESCLASS is already a domain 
> constructor and dependent types for domain constructor is not
> a problem in Axiom. Since RESCLASS is a categorical construct,
> the implementation must NOT know anything about R or M other
> than that R is a commutative ring and M is a maximal ideal of R.
> ...
> 
> The solution I proposed in package FOO:
> 
> > --%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)
> > 
> > )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
> 
> does not sacrifice the mathematical type structure of the 
> original example that Martin proposed:
> 
>    g(n:PositiveInteger, k:PositiveInteger):PrimeField(n)
> 
> It reflects exactly the same structure with the exception that
> there is no signature used and g(n,k) is replaced by the longer
> name point()$Foo(n,k) as illustrated in the Bartest package.
> I do admit that Aldor is nicer to allow that, so that such a
> wrapper is not necessary.  But the wrapper is straightforward
> and general and can even be automated.
> 
> If one MUST use the signature for g (other than it is 
> convenient), then you need Aldor. But can someone supply such
> an example from Aldor?
> 

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.

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.

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?

Regards,
Bill Page.