[Axiom-developer] [#219 The interpreter does not understand dependend types]

[kratt6]

Changes 
http://page.axiom-developer.org/zope/mathaction/219TheInterpreterDoesNotUnderstandDependendTypes/diff
--

??changed:
-
The following Aldor construct does not yet work in Axiom.

This is in fact the reason why I would love to have Aldor working. I did not 
expect it to work, and it does not, but it works *almost*. The code is as 
follows:

\begin{aldor}
#include "axiom"

Test: with { f: (n: PositiveInteger) -> PrimeField(n) } 
   == add { f(n: PositiveInteger): PrimeField(n) == 
              10::Integer::PrimeField(n) }
\end{aldor}

Note that such a construction - the resulting domain depending on the function 
parameter - is currently illegal in Axiom. In Aldor it is fine.

I compiled it with Aldor as usual, and then loaded it into Axiom. As signature 
I got the slightly unusual:
\begin{axiom}
)di op f
\end{axiom}

and trying it out I obtained:
\begin{axiom}
f(5)$Test
\end{axiom}

which is roughly what I expected. However, to my great surprise, if you turn on 
the debugger (beforehand. You always have to start a fresh axiom because of the 
error I told you about in my previous message) with::

  )lisp (setq |$monitorNewWorld| t)

and thus trace::

  f(1783)$Test

the final bit reads::

  protected-symbol-warn called with (NIL)..IntegerMod 1783 wants
   positiveRemainder : (%,%) -> % from  Integer
  ---->Integer----> searching op table for:
   positiveRemainder : (%,%) -> % from  Integer
  <----#<compiled-function |INT;positiveRemainder;3$;28|> Integer
  goget stuffing slot 47 of IntegerMod 1783
  <------#<compiled-function |INT;positiveRemainder;3$;28|> Integer

  PrimeField n activating lazy slot 8: Integer
  PrimeField n activating lazy slot 9: IntegerPrimesPackage Integer

  ..PrimeField n wants
   prime? : Integer -> Boolean from  IntegerPrimesPackage Integer
  ---->IntegerPrimesPackage Integer----> searching op table for:
   prime? : Integer -> Boolean from  IntegerPrimesPackage Integer
  <----#<compiled-function |PRIMES;prime?;IB;4|>(IntegerPrimesPackage,Integer)
  goget stuffing slot 10 of PrimeField n
  <------#<compiled-function |PRIMES;prime?;IB;4|>(IntegerPrimesPackage,Integer)

which clearly tells you, that the calculation is done alright, only the
signature interferes with success.

Any ideas?

Peter said, that it's on the interpreter side. You can read the whole
thread on 
http://lists.gnu.org/archive/html/axiom-developer/2005-01/msg00154.html

Concerning his patches, Peter also pointed out that

- aldor "extend" does not work

- The algebra defined in libaxiom.al is not current, and for it to be rebuilt
  various .as files need to be available to the build process (axextend.as and
  friends)

- exported attributes from aldor domains are explicitly killed off by this
  patch (it's probably easy to fix, just no time at the moment).  

- Only tested the most trivial domains he could find.

--
forwarded from http://page.axiom-developer.org/zope/mathaction/address@hidden