[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
## Re: [Axiom-developer] Functors

**From**: |
Ralf Hemmecke |

**Subject**: |
Re: [Axiom-developer] Functors |

**Date**: |
Wed, 22 Nov 2006 13:40:26 +0100 |

**User-agent**: |
Thunderbird 1.5.0.8 (X11/20061025) |

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