axiom-developer
[Top][All Lists]

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

 From: Ralf Hemmecke Subject: Re: [Axiom-developer] Question concerning types... Date: Sun, 17 Sep 2006 19:58:52 +0200 User-agent: Thunderbird 1.5.0.5 (X11/20060719)

```On 09/17/2006 04:25 PM, Gabriel Dos Reis wrote:
```
```Ralf Hemmecke <address@hidden> writes:

| > | > Intuitively I would expect Variable to mean simply "an
| > | > unspecified specific instance of a Domain/Type/what have you"
| > | > with ALL domains being possible - just so long as you specify
| > | > the type of the variable, e.g.:
| > | > | > a1 : Variable(Matrix Quaternion Fraction Integer)
| > | > | | Suppose there was such a domain constructor named
| > Variable(D: domain)
| > | which had the properties you suggest. What operations would you expect
| > | this  domain to export? Would it have the same operations as D? For
| > | example '+'. Given two objects from the domain Variable(Integer),
| > | say 'x' and 'y', what is the type of the result of 'x+y'? Is it
| > | still in Variable(Integer)?
| > FreeMonoid Variable Integer
```
| | Gaby, do you really believe that? But in order to say x+y you have to
```| have the type of Variable(D: domain) in the first place.

yes.  My working assumption is that if we had Variable(D: domain) to
mean anything, it would be such that operations of D would be *lifted*
to Variable(D: domain) and would work as if we had an algebra (in the
Universal Algebra sense).  In this case "+" would be lifted to
Variable Integer, so that x + y can be interpreted as an element a a
free monoid generated symbols.  That is not rocket science.
```
```
```
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").
```
```
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.
```
```
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).
```
```
Anyway, what we want is a nice way of adding elements and more or less keeping the type of the domain. And that is not possible if you just define "Indefinite" having one argument D. One must know the type of D (a category) so that the return type would be clear.
```
Indefinite(C: Catagory)(D: C): C == add {
Rep == Union(d: D, ???)
...
}

```
The ??? should be something that allows arbitrary expressions formed from D, the functions in C and some indeterminates X. (I have no idea how that would look like. Maybe just delayed evaluation of function composition.)
```
```
```[...]

| (1) -> (a1,a2,a3,a4):Expression Quaternion Fraction Integer
|         Type: Void
| (2) -> m := matrix[[a1,a2],[a3,a4]]
```
| | +a1 a2+
```|      (2)  |      |
|           +a3  a4+
|         Type: Matrix Expression Quaternion Fraction Integer
```
| | given by Bill suggest that the Axiom interpreter is a bit more relaxed.
```
Funny enough, I tried similar thing and sent a message before seeing
Bill's.  That is a natural thing to do if you have a Universal Algebra
backgroud -- e.g. you're used to the 3M's.
```
```
```
Maybe. I don't say that shouldn't be allowed in the interpreter, but the compiler would generate a matrix of 4 uninitialized entries. 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. 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 guess the interpreter has to do a lot of
| work to find the right interpretation for such a + and it must decide
| for one of possibly many choices.

If "+" is defined as beeing an associative operation , there would not
```
be much work to do.
```
```
Oh, who said that + is associative? The documentation, right? But that is not a nice thing to take into account for the compiler. It would be much better if Aldor allowed to state associativity in a formal manner.
```
```
```In fact I don't want the interpret to become
super smart.  Just lift operations.
```
```
```
I am completely with you. The interpreter should not have any mathematical knowledge, just look into a database (basically the Axiom libraries) and figure out what could be done. It should be possible to change the libraries and work with the same interpreter.
```
```
```| But assume I say x+z for
| z: Variable(Float) := "z"
```
| what is the type of that?
```It is the type of its declaration: Variable(Float).
```
```
Oh, I meant the type of "x+z".

```
```| Should the interpreter forbid such an
```
```
```
```there is no addition as far as I can see.
```
```
```
But there was also no addition until you transformed Variable(Integer) into FreeMonoid Variable Integer.
```
```
```| In the compiler I clearly don't want any guessing and not
| automatic conversion. Note that I prefer that (most of) the things
| that are possible in the interpreter could be compiled into stand
| alone programs.
| Anyway, if the type tower is always expanded like that  you end up
| with the fact that
| (x+y)*x and x*x + x*y
| have types
| and
| and thus are not equal.

I don't see why.
```
```
OK, let's turn this into a mathematical example.

A := Fraction Complex Integer; a: A := 1
B := Complex Fraction Integer; b: B := 1

Clearly A and be are isomorphic as fields, but they are NOT identical.
Not identical in Axiom and not identical in mathematics.

```
Note, we had a discussion whether "Fraction Fraction Integer" should be implemented to be the same as "Fraction Integer". Although I had even given code to do that, I believe it should not be implemented that way. Because an element that looks like (2/1)/(3/1) is NOT identical to 2/3. (Just consider fractions as equivalence classes of pairs of some type.
```
Ralf

```