Ralf Hemmecke <[EMAIL PROTECTED]> 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 _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer