On Tue, Aug 5, 2008 at 9:26 PM, Gabriel Dos Reis wrote: > Bill Page writes: > | > | Ok. What do you think of this solution (passing symbols) that I have > | been discussing with Ralf? > | > | http://axiom-wiki.newsynthesis.org/SandBoxAbelianDuck > | > | )abbrev category ASSOC Associative > | ++ m(m(a,b),c) = m(a,m(b,c)) > | Associative(m:Symbol):Category == with > | m:(%,%) -> % ++ multiplication > > > I think I already offered my opinion about this when we were in > Hagenberg. My problem with this is that it associate the associative > property with a symbol, not an operation.
That is not how I interpret the above code. In fact, if I write: MyDomain(): Associative("*") The compiler does generate code with *:(%,%) -> % The associative property is associated with the category 'Associative("*")' but *:(%,%) -> % is exactly what is exported by this category so it is precisely that map to which this property applies. > That is a problem because an operation is not just an symbol. An > operation is described by a name, a domain of computation (or package) > and its signature. Yes. That is exactly what I see above. > Otherwise, one gets into the same trap as the M&M who as able to > evaluate M * N - N * M to *integer* 0, no matter what M and N might > be. I don't see that happening here. Could you explain? > > I believe I already sketched a solution that I'm working on (I hoped > Yixin would pick it up, but that is not coming). It realies on the > notion of `modemap'. So in the typical System F/AXIOM style, > I would write the above as > > Associative(T: Type, Modemap(T,T,T): op): Category == with nil You meant? Associative(T: Type, op:Modemap(T,T,T)): Category == with nil > > There is no export because associativity is essentially a logical > axiom. All category declarations are "logical axioms" in this sense. > > In Implicit System F, or in a forall-quantified style I would write > > forall(T: Type) . > Associative(Modemap(T,T,T): op): Category == with nil > > so that when I say Associative(_+$Integer), T gets deduced to > Integer. You can see how this relates to the issue Stephen and > I discussed at the workshop in Hagenber. > Yes, I thought it was an interesting discussion but this machinery strikes me as being to "heavy" for what seems to me to be a relatively simple problem. I am afraid that such changes lead away from the original intend of Spad/Aldor as fundamentally an *algebraic* language. But my ideas about this are only partially formed, so I do want to keep an open mind. > | --------- > | > | where the compiler does already replace 'm' with the symbol passed > | as an argument. The problem with this approach actually occurs at > | a later stage in the compilation where the parameter occurs to the > | right of the ==. E.g. > | > | )abbrev category ID Identity > | ++ m(u,a)=a and m(a,u)=a > | Identity(u:Symbol,m:Symbol):Category == Commutative(m) with > | u: () -> % ++ unit > | > | ------- > | > | Somewhere else we get the complaint: > | > | >> System error: > | |Identity;| [or a callee] requires more than one argument. > | > | -------- > | > | Is the cause clear to you? > > I have to have a complete working system to get my head around the > problem. > Is there something more that I could provide you that is not included on the above mentioned web page? > | > | I recall Stephen Watt's comment during the recent workshop that > | they (meaning the ScratchPad project I presume) tried to make > | this sort of solution work but abandoned it for reasons which he > | did not elaborate. Do you have some ideas about what these > | reasons might have been? > > In fact, as it turned out at the workshop Stephen was also solving > that same problem; but from a different angle; I'm not sure he > abandoned. I think we did not finish the discussion -- but I > mentioned that I was solving it by making modemaps more real; > he observed that also permits ML-style polymorphism. > Yes, that is what I referred to above as a "heavy non-algebraic" kind of solution. I am sorry to use such a vague characterization. Maybe I will be able to do better at some time in the future. I took that fact that this approach of passing symbols that are evaluated as names of exported functions "almost works" as evidence that some changes were made to Spad that were intended to make this possible. (Why else evaluate the function names?). It seems to me that the bug that prevents its full use in the "monoid problem" is not a fundamental design problem but rather something much more technical. I would greatly appreciate any suggestions you have about how to approach debugging this problem. Regards, Bill Page. ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel