Re: [Axiom-developer] Question concerning types...

[Ralf Hemmecke]

On 09/19/2006 06:25 PM, Bill Page wrote:
> > > It is certainly a wrong design to implement indefinite integers
> > > as
> > polynomials.
> >
> > Why?
> >
> > Suppose you have a nice algebra library and you want the system to
> > understand indefinite objects, then you are certainly not going to
> > add any function to existing domains or wrap one (and actually ALL)
> > domains with a domain constructor "Indefinite". No. It should be
> > completely transparent.
>
> I am not really sure I understand what you mean by "transparent" -

OK, maybe transparent is a bad word. What I mean was that if I would
like to work with indefinite integers I would not like to write anything
more complicated than "n: Integer". I believe that the type of an
indefinite integer is Integer and NOT Indefinite(Integer). But, of
course that can only work in the interpreter and not in library code (ie
for the compiler).

> particularly in to the context of SPAD/Aldor. For the most part the 
> type system of SPAD/ALDOR is not "transparent" by design.

Here *I* don't understand what you mean by transparent. But it's not
important here.

> One must specify (almost) all types for these compilers. Unlike
> Haskell, for example, type inference in Aldor is very limited.

In terms of readability of the code, I rather like that Aldor forces the 
programmer to add type declarations in function definitions. I agree 
that it is sometimes quite cumbersome, but a bit of redundancy is never 
bad if you read your (own) code in 5 years. We still have no good tool 
that shows the type of identifiers if you hover over it with your mouse.

> Polynomials are necessarily involved in the definition of the 
> LocalAlgebra. Your argument is not an argument against using a 
> LocalAlgebra as an implementation of indefinite integers.

I'll be quite until I have put my ideas into code. Currently I don't 
think that I would use polynomials. I would rather encode an indefinite 
object by a function similar to typed lambda calculus. An indefinite 
integer is then just an identity function Z->Z (macro Z==Integer) and 
addition would be something like

(a: Z->Z) + (b: Z->Z): (Z,Z)->Z == (x: Z, y: Z): Z +-> a(x) + b(y)

the zero? function would be lifted like

zero?(a: Z->Z): Z->Boolean == (x: Z):Boolean +-> zero?(a(x))

But that is all not very well thought of, since how would I then write 
the equivalent of "zero?(2+3)" if 2 and 3 are replaced by indefinite 
integers? Ah, actually one needs

zero?(a: T->Z): T->Boolean == (t:T): Boolean +-> zero?(a(t))

But how to deal with the type T? I stop here.

> > The goal is to type
> >
> > n: Integer;
> >
> > and not
> >
> > n: Indefinite(Integer);
> >
> > Either the interpreter or some layer between interpreter and
> > library code should take care about indefinite objects.

> This could be easily achieved in the Axiom interpreter but I don't 
> think it makes any sense in the compiler. In the compiler you must 
> write:
>
> n: Indefinite(Integer)
>
> (or the equivalent) because of the semantics associated with
>
> n: Integer
>
> in a static strongly typed language.

Right. But I need a use case that would justify that it is reasonable 
that indefinite integers should appear in library code.

> > I very much believe that this requires reflection from SPAD/Aldor.

> Why? I do not see reflection as essential in a statically typed 
> language.

Oh, of course, reflection is not generally necessary. I meant that for 
what I have in mind I probably would need reflection. But maybe not.
Don't take me too serious. All that discussion is just to make the 
concept clearer. Code is still far away, especially a good design for 
indefinite objects.

Ralf