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

[Gabriel Dos Reis]

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.

[...]

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

[...]

| 2)
| Now Gaby said that x+y should have type FreeMonoid Variable
| Integer. Why not FreeGroup?

I picked FreeMonoid because that is the least assumption with "+" from
Integer.  But I'm OK to have the interpereter go directly to FreeGroup
-- that would be even more consistent with my earlier suggestion of
lifting operations to Variable D.

| 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.  In fact I don't want the interpret to become
super smart.  Just lift operations.

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

| Should the interpreter forbid such an
| addition?

there is no addition as far as I can see.

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

| And what would be the type of foo?(x,y)? Maybe I have extended Integer
| to contain a function foo: (%, %) -> Boolean. 

Yes, what is the resulting Algrbraci structrure?

| Variable(Integer) does
| however not export anything about its argument.

it does not have to.

| So who is going to find out that such a foo exists?

The process would be that of lifting operations from D to Variable(D).
Notice, this isn't a problem for programming languages.  Think about
it from Universal Algebra perspective.

-- Gaby