[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Axiom-developer] Functors

From: Waldek Hebisch
Subject: Re: [Axiom-developer] Functors
Date: Wed, 22 Nov 2006 13:16:21 +0100 (CET)

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:
> ml
> 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

reply via email to

[Prev in Thread] Current Thread [Next in Thread]