[Aldor-l] [Axiom-developer] spad: language and compiler

[William Sit]

On 24 Aug 2006 14:38:19 +0200
  Martin Rubey <martin.rubey at univie.ac.at> wrote:
>Ralf Hemmecke <ralf at hemmecke.de> writes:
>
>> > f(m: INT, n: INT): PF n == m::PF(n)
>that's OK.
>
>
>> > [f(100, n) for n in primes(1,100)]
>that's stupid.

Why? I would think it is an element (not a list) in a 
cartesian product of #primes(1,100) prime fields.

>> Ask yourself, what type that list will have and you 
>>realise that Aldor will
>> reject that its compilation.
>Excuse me, Gaby. Sorry about being so stupid.

It's a perfectly good mathematical object in a cartesian 
product.

>
>> > [a::P for P in L]
>> That is as problematic as the first list.
>"problematic" is an understatement. Sorry.

Ditto. The only problem I see that can't be handled is if 
you make it into a function of k:

[f(100, n) for n in primes(1,k)]

To have true dependent types means the compiler should be 
able to handle

[f(100, n) for n in primes(1,100)]

because the list primes(1,100) is computable at compile 
time and hence the prime fields can be constructed and 
their cartesian product too. prime(1,k) is a totally 
different ball game, but even that should be doable with 
generated code to instantiate the prime fields when k is 
given a value at run time.

William