axiom-developer
[Top][All Lists]

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

 From: Ralf Hemmecke Subject: Re: [Axiom-developer] Question concerning types... Date: Mon, 18 Sep 2006 13:23:50 +0200 User-agent: Thunderbird 1.5.0.5 (X11/20060719)

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
```
```
```
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

```