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

[Ralf Hemmecke]

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
> | addition?

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