Re: [Axiom-developer] "has" and "with"

[Gabriel Dos Reis]

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