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

[Gabriel Dos Reis]

On Thu, 16 Aug 2007, Ralf Hemmecke wrote:

[...]

| You cannot achieve that uniformity. Take
| 
| define Cat: Category == with;
| define Foo(T: Cat): Category == with {};
| DomI: Foo(Integer) == add;
| DomS: Foo(String)  == add;
| b1: Boolean == DomI has Foo(Integer);
| b2: Boolean == DomI has Foo(String);
| b3: Boolean == DomS has Foo(Integer);
| b4: Boolean == DomI has Foo(String);
| 
| If you treat domain constructors in the same way as basic values (functions)
| then
| 
|   Foo(Integer) = Foo(String) = with {}

How is the above is a logical consequence?  
In no way I have tied argument passing semantics to equality.

| So b1, ..., b4 should all be true, right? But I remember faintly that you
| argued about a functional language with respect to the types and that you
| would like to be able to distinguish
| 
|   Foo(Integer) from Foo(String)
| 
| No?

For sure, I would like to distinguish those two.  However, I do not
see how that follows from the semantics of passing arguments in function
calls. 

| Where would be the uniformity here?

The uniformity is in terms of prerequsite of instantiation -- same rules for
everybody. 

-- Gaby