On Thu, 16 Aug 2007, Ralf Hemmecke wrote: | > Whether those those two categories are equal in the sense that | > "=" returns true is entirely a matter semantics attached to | > the "with"-construct. There is no predefined choice. | | Yes, I understand and agree. I don't even remember that I have seen clearly | that I have seen a statement in the AUG that says that | | with {} | | and | | with {} | | would necessarily two identical or non-identical things. Maybe that should be | considered a bug in the documentation. | | And that Foo(Integer) is different from Foo(String) but equal to Foo(Integer) | you can only assure if the language restricted to types is functional.
Hmm; I'm lost. Could you elaborate on the last paragraph? | We all know that one could define | | define Bar(i: Integer): Category == with; | | and here I am no longer sure whether Bar(0) is really treated differently (by | the current aldor compiler) from Bar(1) in a "has" construct. I'd like to have | the same behaviour as for type-valued arguments, but maybe there is some good | reason why the Aldor compiler behaves different for non-type-valued arguments. | There must be some examples on this list, I just don't know how I can find | them now. In any cas,e it would be nice to have those examples, and the logical inference rules that go with them put somewhere for future reference. [...] | > | So my guess was that they should be treated in the same way. | | > Well, ne need rules to define equality on objects we manipulate | > in programs. Every definition has its consequences -- pros and cons. | | Good. Where should these pros and cons go to? Any suggestion for a | documentation. MathAction? I believe MathAction is a good place to start. (But, I tend to leave on emails...) | > In the field of type theory, the notion of equality on types (and modules) | > is a fertile area of research that has been going on for ages. | > Search for "manifest types" and "generative types". Youcan replace | > "type" by "modules". | | Thank you. I'll do my homework. | | > My point of view is this: I believe the idea of treating category, | > domain, and packages instantiation as function call is a good uniform rule. | > I also believe that we should further uniformity by | > having only one set of rules for function calls -- e.g. we don't | > have one rule for values, one for types, and one for whatever. | | If that can be done, I am all for it. | | > Notice that, in that view, the notion of value equality is not involved. | | Hmmm, but doesn't that mean that whether baz(0) is equal or not equal to | baz(1) has nothing to do with the implementation of "=" in Integer? That | sounds a bit strange to me. What are contexts (examples) where =$Integer would | not be needed? Well, there are two things here: * evaluating the expressions "baz(0)", "baz(1)", "baz(x)" where x is a variable * evaluating the expression "baz(0) = "baz(1)" what I'm saying is that in the evaluation of the function calls baz(1), baz(0), baz(x), I don't see where the definition of =$Integer is involved. Nor, am I sure it should be involved -- utimately we would like =$Integer to be a function itself that can be called... -- Gaby _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer