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

[Ralf Hemmecke]

Thank you for your answers that was better.
May I continue.

Gabriel Dos Reis wrote:
> 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.

Of course.

> | 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 ("{ }")

I haven't stated anything else above. Just that I did not say "another".

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

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.

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

I completely agree.

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

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

Ralf