Re: [Axiom-developer] Functors

[Ralf Hemmecke]

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

If that works with the spad compiler then why is there a belief that the 
spad compiler cannot handle dependent types?

Maybe the problem is that spad doesn't allow

g(p:PositiveInteger, k:Integer):PrimeField(p) == ...
???

Clearly the result type of g(p,k) depends on the input value of g.

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

What syntax are you speaking about? I cannot see, why what Bill wrote is 
not Aldor 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.

I don't understand that. But would you allow something like that in SPAD 
(not the interpreter)?

p: Integer := 5;
k: Integer := 17;
kmod5: PrimeField(p) := k :: PrimeField(p);
p := foo(p); -- results in p=7
kmod7: PrimeField(p) := k :: PrimeField(p);
kmod7 := kmod5 + kmod7

In order to type check that piece of code you need compile time 
evaluation of foo. That is the reason why Aldor requires parameters of 
types to be constant in the given context.
That has nothing to do with "dependent types" though.

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

Do you use "dependent type" as in

http://www.aldor.org/docs/HTML/chap7.html#4

?

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

Could you elaborate on this?

Ralf