Re: [Axiom-developer] Functors

[Waldek Hebisch]

Bill Page wrote:
> On Wednesday, November 22, 2006 4:35 AM Frederic Lehobey wrote:
> >     PrimeField(7)
> > 
> > and
> > 
> >     PrimeField(p)
> > 
> > both work in interpreted mode whereas the second one is not compiled
> > by the old compiler (it has already been discussed some time -- years
> > -- ago on axiom-dev).
> >
> 
> Are you referring to the discussion of dependent types in Aldor function
> definitions such as
> 
>   g(p:PositiveInteger,k:Integer):PrimeField(p) == k::PrimeField(p)
> 
> This looks innocent and "natural" in Aldor, and in the Axiom interpreter
> but William Sit and Ralf Hemmecke showed that in fact this is not really
> a function definition in the sense of category theory at all but rather
> a functor (i.e. package or domain constructor). See:
> 
> http://lists.nongnu.org/archive/html/axiom-developer/2005-01/msg00207.ht
> ml
> http://lists.nongnu.org/archive/html/axiom-developer/2005-01/msg00310.ht
> ml
> 
> In the Axiom/SPAD compiler you can write such a functor as
> 
> g(p:PositiveInteger, k:Integer):with point:()->PrimeField(p)
>   == add point()==k::PrimeField(p)
> 
> The function 'point' is necessary because a functor returns something
> of type category. The parameters pick out a particular function from
> the category. E.g.
> 
>   point()$g(7,4)
> 
> > ...
> 
> >From my point of view this is technically more correct than Aldor's
> syntax.

I must disagree here: main feature of dependent types is that they
depend on parameters -- one can say that normal types depend only
on constants.  Axiom goes half way here: it allows dependence on
parameters, but only if parameter is a "category/domain/package 
constant", that is you can only use expressions depending on constants
and constructor parameters as parameters for dependent types.

"Full support" for dependent types would require more forms (
function parameters, record fields).  From the point of view of
category theory you may be forced to introduce extra functors,
but I would say that whole point of dependent types is to hide
the extra machinery.

-- 
                              Waldek Hebisch
address@hidden