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

[Ralf Hemmecke]

> | > 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
FreeMultiplicativeSemigroup FreeAdditiveSemigroup Variable Integer
and
FreeAdditiveSemigroup FreeMultiplicativeSemigroup Variable Integer
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