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 09:28:34 +0200 User-agent: Thunderbird 1.5.0.5 (X11/20060719)

```| > 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. So let's
suppose you simply say (Aldor-speak: PrimitiveType exports just equality)

Variable(D: PrimitiveType): PrimitiveType == add {
Rep == ...
(x: %) = (y: %): Boolean == ...
}

So you actually say that Variable is rather thumb. But first you have to
create x and y. So you would say

x: Variable(Integer) := "x"  -- give the name of the symbol
y: Variable(Integer) := "y"

There are already two issues here.

1)
When you just say
x: Variable(Integer)
without the assignment, you just declare an (Aldor/Axiom) identifier, no
value yet. If ever you are going to compute with x it has to have a
value. Now actually the domain Symbol does exactly that. However the lines

(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.
```
It actually interprets a1 as both, an Axiom identifier and as a variable of the domain Expression Quaternion Fraction Integer.
```
Try

b: Expression Quaternion Fraction Integer := B
B

in Axiom.

2)
```
Now Gaby said that x+y should have type FreeMonoid Variable Integer. Why not FreeGroup? 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. But assume I say x+z for
```z: Variable(Float) := "z"
```
what is the type of that? Should the interpreter forbid such an addition? 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.

```
And what would be the type of foo?(x,y)? Maybe I have extended Integer to contain a function foo: (%, %) -> Boolean. Variable(Integer) does however not export anything about its argument. So who is going to find out that such a foo exists?
```
Ralf

```