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
[EMAIL PROTECTED]
_______________________________________________
Axiom-developer mailing list
[email protected]
http://lists.nongnu.org/mailman/listinfo/axiom-developer
