[Axiom-developer] Re: [Axiom-mail] Function returning UnivariateTaylorSeries

[Stephen Wilson]

Hello,

I would like to give a final overview of what I have uncovered
regarding this dependent typing issue. Unfortunately the problems it
raises are quite extensive.

We could solve the initial problem wrt Marcus's Foo domain. The
problem is with the interpreter not performing type analysis on the
signature of the bar function:

     bar(): () -> UnivariateTaylorSeries(K, z, 0)

Eventually the signature itself is rewritten inside the interpreter,
but only the parameters from the domain Foo(K, z) are analyzed. The
0 is left untouched. 

It is possible to extend the interpreter to solve the class of
problems which this example represents. It amounts to writing some
code which performs coercions on signature parameters.

However, it is easy to come up with variations on the Foo domain which
would not be addressed. Here are two particularly troubling examples:

================================================================
)abbrev package FOO1 Foo1

Foo1(K, z): Exports == Implementation where
  K : Ring
  z : Symbol
  Exports == with
    bar1: () -> UnivariateTaylorSeries(K,z,0);
  Implementation == add
    bar1(): UnivariateTaylorSeries(K,z,0) ==
      st := generate(const(1)$MappingPackage2(K, K),0)$Stream(K)
      series(st)$UnivariateTaylorSeries(K,z,0)

)abbrev package FOO2 Foo2

Foo2(K, z): Exports == Implementation where
  K : Ring
  z : Symbol
  Exports == with
    bar2: K -> Stream K
  Implementation == add
    bar2(x: K): Stream K ==
      F := Foo1(K, z)
      uts := bar1()$F
      eval(uts, x)
================================================================

The Foo2 domain simply will not compile:

================================================================
   Compiling AXIOM source code from file /home/steve/tmp/foo2.spad 
      using old system compiler.
   FOO2 abbreviates package Foo2 
------------------------------------------------------------------------
   initializing NRLIB FOO2 for Foo2 
   compiling into NRLIB FOO2 
   compiling exported bar2 : K -> Stream K
****** comp fails at level 1 with expression: ******
error in function bar2 

(0)
****** level 1  ******
$x:= 0
$m:= K
$f:=
((((|uts| #) (F #) (|last| #) (|rest| #) ...)))
 
   >> Apparent user error:
   Cannot coerce 0 
      of mode (NonNegativeInteger) 
      to mode K 

protected-symbol-warn called with (NIL)
================================================================

This implies that even if we were to extend the interpreter to handle
`signature coercions' we would still not be able to use our domains
for general library development, as this is a compiler issue.


Another example is the following variation on the original Foo:

================================================================
)abbrev package FOO3 Foo3

Foo3(K, z): Exports == Implementation where
  K : Ring
  z : Symbol
  Exports == with
    bar3: (c:K) -> UnivariateTaylorSeries(K,z,c);
  Implementation == add
    bar3(c:K): UnivariateTaylorSeries(K,z,c) ==
      st := generate(const(1)$MappingPackage(K, K),c)$Stream(K)
      series(st)$UnivariateTaylorSeries(K,z,c)
================================================================

Trying to compile a domain which uses Foo3 will fail. 

Trying to use Foo3 directly will invoke a problem in the interpreter
similar to the one invoked by Foo1. The problem is more severe in this
case since the signature is:

   bar3: (c:K) -> UnivariateTaylorSeries(K,z,c)

As before, K and z will be properly rewritten w.r.t the domain
parameters. Whats left for the interpreter to deduce is what the
symbol 'c' means. As far as I can tell, this information is simply not
available. The database information produced by the compiler gives
type information for bar3's arguments -- nothing with respect to
the binding of symbols to formal parameters. 

Interestingly, the compiler generates a file `info', which for Foo3
looks like this:

================================================================

((|bar| (((|UnivariateTaylorSeries| K |z| |c|) K)
         ((|UnivariateTaylorSeries| K |z| |c|)
          (|series| (|UnivariateTaylorSeries| K |z| |c|) (|Stream| K))
          (|One| (|UnivariateTaylorSeries| K |z| |c|)))
         ((|Stream| K) (|generate| (|Stream| K) (|Mapping| K K) K))
         ((|MappingPackage2| K K) (|const| (|Mapping| K K) K))
         (|locals| (|st| |Stream| K)) (|arguments| (|c| . K))
         (K (|One| K))))) 

================================================================

Notice the `(|arguments| (|c| . K))' form. I am not sure when or how
this info file is used, but it does contain the information we would
need. A general solution to this problem would probably involve an
extension to the database such that the formal argument bindings are
available to the interpreter.

Clearly, tackling this problem would require a solid understanding of
both the compiler and interpreter -- something I do not posses.

I will keep these issues in mind as I learn more about axioms
internals. 

Perhaps down the road there could be an axiom-langextension-1 branch
which could serve as a playpen for exploring and formalizing axioms
dependent type system.


Sincerely,
Steve