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

[Gabriel Dos Reis]

Ralf Hemmecke <address@hidden> writes:

[...]

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

yes.

| Mathematically, that's not a big deal. But Aldor domains are actually
| multi-sorted algebras. That makes the situation a little more
| complicated.

but not impossible.

In this discussion, I'm going to ignore Aldor for a moment and
concentrate on SPAD because I don't have access to Aldor source code
and anything that might transpire out of this discoussion should 
probably be recorded as a feature-request for SPAD with all the
"insights" we might have gained.

| 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).

I don't think it should be Variable(Integer).  For me,
Variable(Integer) means a symbol who interpretation is of type
Integer.  I don't like Indefinite(Integer) neither.  So, it might very
well be that we're back to our old beloved friend Expression(Integer).

| Anyway, what we want is a nice way of adding elements and more or less
| keeping the type of the domain.

yes.

| And that is not possible if you just define "Indefinite" having one
| argument D. 

I'm clear why not.  Could you explain this a bit further?

| 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.)

I suspect I'm being dense here.  What would be wrong with Expression D?

| > [...]
| > | (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 entry is a Variable? I would expect the output to indicate
either the name or just m(1,1).  Look at what Axiom prints when you
say

    m * m

That matches my expectation.

| 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)"? 

well, it Expression is dropped then we're back to the interpretation
we all agree on: A value of type Quaternion Fraction Integer.
Consequently m(1,1) must hold value of that type.

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

And

yes, but in my model much of the documentation is moved to code.  In
this case, I would like to see properties() used to attach
mathematical properties.  

| But that
| is not a nice thing to take into account for the compiler.

Why?  

>From my point of view, the type of an operation is just as important
as its algebraic properties.

| It would be
| much better if Aldor allowed to state associativity in a formal manner.

SPAD does.  See properties()

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

yes.

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

I did not transform a variable to FreeMonoid Variable Integer.
However, I did suggest that type  for th _compound expression_ "x+y"
when the question was asked.

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

As syntactic obejcts, no, they are not.  The issue can be rephrased as
whether they should remain non-equal in other non-syntactical
intepretation.   I think no.

| Not identical in Axiom and not identical in mathematics.

You have lost me on the last part.  My book says that both A and B are
the same mathematical object.  Why do you believe they are not?

| Note, we had a discussion whether "Fraction Fraction Integer" should
| be implemented to be the same as "Fraction Integer".

Under the mathematical interpretation they are the same.  I believe
they should also be the same in Axiom -- at least if you take
dependent types seriously.

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

By the same token we should prevent Axiom from simplifying 3+2 to 5.

| (Just consider fractions as equivalence classes of
| pairs of some type.

I don't follow.

-- Gaby