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

[Gabriel Dos Reis]

On Thu, 16 Aug 2007, Ralf Hemmecke wrote:

| Gabriel Dos Reis wrote:
| > On Thu, 16 Aug 2007, Ralf Hemmecke wrote:
| > 
| > | > |   Foo(Integer) = Foo(String) = with {}
| > | > 
| > | > How is the above is a logical consequence?  In no way I have tied
| > | > argument
| > | > passing semantics to equality.
| > | 
| > | What does that have to do with "argument passing semantics"?
| > 
| > That was my question.
| 
| Thank you. Your answer is quite helpful to me. :-(

Ralf --

   It wasn't an answer.  It was a genuine question that I asked in
the mail you were replying to.

| > | Foo is a function and the resulting values of Foo(Integer) and Foo(String)
| > | are
| > | the same.
| > 
| > Why?
| > 
| > 
| > | Very much like foo(0) = foo(1) for
| > | foo(i: Integer): Integer == 1.
| > 
| > but 1 is not String, 1 is not Integer.
| 
| Maybe you didn't realize that I wrote foo not Foo.

"foo" was a tupo.

| Let me repeat.

I got what you were saying, but it seems to me that you were making
an implicit assumption on "=" that is in no way related to argument
passing.

| define Cat: Category == with;
| define Foo(T: Cat): Category == with {};
| DomI: Foo(Integer) == add;
| DomS: Foo(String)  == add;
| baz(i: Integer): Integer == 1;
| 
| I have two functions Foo: Cat -> Category and baz: Integer -> Integer.
| 
| Clearly, baz(0) evaluates to 1 and baz(1) also evaluates to 1.

So far, I agree.


| Both values are equal with respect to "=" (used with the semantics
| defined in Integer).

Bingo!  Here, you're using "=" from the Integer.  If that operation
were defined to always return false, then you would have reached a
different conclusion.

| The argument simply doesn't matter.

OK.

| Now Foo(Integer) evaluates to
| 
|   with {}
| 
| and Foo(String) evaluates to
| 
|   with {}

I don't think I agree here.

For me:

  *  Foo(Integer) evaluates to a category with empty body ("{ }")
  *  Foo(String) evaluates to another category with empty body ("{ }")

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.


| There is not definition of equality between categories,
  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

It is very important to realize this and spell it out clearly.
Because, there is no fundamental reason why there is none.

| but here the even look identical.
                    ^^^^

"Looking" is not the same as being equal.  


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

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

| My guess therefore is that
| 
|   DomI has Foo(Integer)
|   DomI has Foo(String)
|   DomI has (with {})
| 
| should all return the same value, namely true. Again if treated
| uniformly with the baz function above, the argument to Foo should not
| matter. But it does, and perhaps that is even good.
| 
| > | So b1 ... b4 should all be true and
| > | 
| > | Foo(String) is indistinguishable from Foo(Integer).
| > 
| > I'm missing the logical reasons for that.
| 
| Hmmm, sorry, I seem to annoy you.

You're not annoying me.  I'm trying to get all implicit assumptions 
spelled out clearly so that they can be properly analyzed.  In particular,
the compiler will be performing the task as a logical chain of steps.

| Anyway, I'll stop explaining things if
| I don't get any good explanation of your point of view in return.

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.

Notice that, in that view, the notion of value equality is not involved.

-- Gaby