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

[Ralf Hemmecke]

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

> | 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.
Let me repeat.

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.
Both values are equal with respect to "=" (used with the semantics
defined in Integer). The argument simply doesn't matter.

Now Foo(Integer) evaluates to

  with {}

and Foo(String) evaluates to

  with {}

There is not definition of equality between categories, but here the
even look identical. So my guess was that they should be treated in the
same way.

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. Anyway, I'll stop explaining things if
I don't get any good explanation of your point of view in return.

Ralf