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

[Ralf Hemmecke]

> > I agree with you that if D had type T then Variable(D) should 
> > have type T (plus maybe some exports that allow to create
> > "indeterminates").
>
> The meaning of this statement is unclear to me. Do you mean:
> If D has category T then Variable(D) should have category T?
> If so, I would disagree. Variable(D), as a universal algebra
> over some symbols must have a different (but related) type,
> perhaps Variable(D) has Universal(T)?

Let's make it simple. Integer is a Ring. Don't you want that Integer 
together with "indefinite integers" also form a ring? I don't think that 
I would want Universal(Ring). What is Universal, by the way?

I understand that "indefinite" thing just as a way to encode a delayed 
evaluation. In the "computation" that is done just with the type 
information, you can do any tricks that you can do with that 
information, but if that computation needs a value, it has to wait until 
I provide one. The point is, that you cannot apply an arbitrary 
operation on these indefinite objects. For example if I have a very 
restricted scope and not / operation can be seen then the compiler 
should reject to compile a/b for indefinite integers a and b.

> > Looking at it mathematically (and simplified) then all we do 
> > is that we take a universal algebra D = (A, F) where A is the
> > carrier set and F are the functions on it. Variable(D) is maybe
> > a bad name, but all we do is that Variable(D) = (A', F') is a
> > universal algebra where A' is the union of the set A, a set X 
> > of indeterminates, and all things that can be generated from A
> > and X by applying functions from F'. F and F' behave identically
> > on A.
> >
> > Mathematically, that's not a big deal. But Aldor domains are
> > actually multi-sorted algebras. That makes the situation a little
> > more complicated.

> I think sometimes you think too much about Aldor and not enough
> about Axiom... ;)

I don't think that my statement is much related to Aldor. You could 
replace Aldor by Axiom or SPAD, if you like. So what did you actually mean?

> > So I still disagree with you that x+y should be of type 
> > FreeMonoid(Variable(Integer)). From what I said above, it seems
> > more natural to me that its type is Variable(Integer) (well,
> > it's a bad name, maybe Indefinite(Integer) would be better).

> The interesting thing to me is that all you appear to be doing here
> is "re-inventing" the Expression domain constructor.
>
> It seems to me that 'Expression(Integer)' is a good enough name. :-)

But inside Expression(Integer) the variables have NO type information 
attached.

> I strongly recommend that you take a close look at how Expression is
> implemented in the Axiom library.

Thank you. But Expression is not what solves the "indefinite" problem.

> 'sin(a1)' which are not evaluated any further in the Expression
> domain.

OK, let's take

n: Expression Integer := n
z := sin(2* %Pi * n)

Axiom knows, in fact, nothing about the n. But if it really knew that n 
is an Integer, it could simplify z to 0.

That should be a test case for indefinite computation.

> > Now what happens if you print m(1,1)? If that prints something 
> > reasonable then it tells me that the compiler knows about a special
> > domain constructor, namely Expression.
>
> Yes.
>
> > Drop "Expression" from above, what would be on screen for "stdout
> > << m(1,1)"? The interpreter can add smart things. I am asking for
> > the compiler.
>
> I don't understand. Obviously Expression is a domain that the SPAD
> compiler understands. Implementing Expression in Aldor should be
> quite straight forward.

Of course the Expression type is known. But is should not be built-in 
into the compiler. It should live in a library.

Ralf