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


>From my point of view this is technically more correct than Aldor's

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


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


reply via email to

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