Re: [Axiom-developer] Polynomials, abstract objects, provisos

[Ralf Hemmecke]

> One could then create an IndefinitePolynomial over the
> IndefiniteIntegers which exports operations that remain
> in IndefinitePolynomial.

I believe nobody wants that approach. I have just tried to build an 
example of IndefiniteIntegers. Suppose you have found a good data 
representation for it, then what type would you expect the zero? 
function has? The only think I can think of is

zero?: % -> IndefiniteBoolean;

So you end up in building always a domain and its indefinite 
counterpart. That is surely unmanageable.

> Unfortunately this method has two problems.
>
> First, it implies either copies of domains such as
> IndefiniteInteger or it implies that you figure out
> how to build an "Indefinite" domain that lives in the
> type tower such as:
>
>    Polynomial (Indefinite (Integer))
>    Indefinite (Polynomial (Integer))
>    Indefinite (Polynomial (Indefinite (Integer)))

I like your second approach better, but after I thought a bit about it, 
I believe that you cannot do this without reflection.

What would be the type of the function "Indefinite"? Clearly it should 
accept any domain. So it would be (T: Type) -> ResultType.

The result type should, however be identical to the (dynamical) type of 
T. Since Indefinite(Integer) should allow any integer operation and 
Indefinite(Boolean) should allow any operations that is defined in 
Boolean. So we would have ...

Indefinite(T: Type): TypeOf(T) == add {...}               -- (*)

So we are out of business here.

Another approach I could think of is that one works with objects (values 
that know its type). One can simulate that in Aldor, too. (Look at 
chapter 21.10 "Objects" in the pdf version of the AUG.)

But again, how would you write "obj1 + obj2"? You must lookup what + 
could actually mean. At compile time you have no chance. So the whole 
business is something for an interpreter. And then (for the interpreter) 
I believe something like (*) should be possible.

> My thinking at the moment leads me to carry the information
> in the proviso as in
>
>    x provided (..... (x is Integer) ....)
>    x provided (..... (x is Polynomial(Integer)) ....)

I somehow think that (*) and your proviso approach are very similar. The 
x basically is like a typed variable (that has no value).

So what should be built is a "typed expression tree" where the leaves 
are typed variables that have no values and the inner nodes are 
functions that wait for their arguments to become actual values.
Whenever a all arguments of a inner node (=function) are actual values, 
then the subtree collapses to an actual value.

I have not yet an idea how to treat a multivalued result.

Any other ideas?

Ralf