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:
| > 
| > | > 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 certainly agree that Foo(Integer) could be but need not be equal to
| Foo(String) since that depends on the definition whether the above two "with"
| expressions should be considered equal or not. That should clearly be
| specified and we are done.

Yes, I agree.

| Now you surely want
| 
| Foo(Integer)
| 
| and
| 
| Foo(Integer)
| 
| (in a reasonably close context) to refer to the same thing otherwise...

I also agree with that.

| In
| 
| if Integer has Foo(Integer) then ..
| if Integer has Foo(Integer) then ..
| 
| you probably don't want to evaluate Foo twice.

In fact, you could evaluate it twice.  The first time, it could setup
a timestamp saying that it is evaluated.  The second time, it would
just return the previously evaluated type.  See the very nice recent work
of dreyer on that subject

   http://portal.acm.org/citation.cfm?id=1090189.1086372
  
using what he called "destination-passing" evaluation strategy.


| (But actually the Aldor
| compiler should since here Foo(Integer) does not appear in "type context" (AUG
| Section 7.3).)
| 
| At the moment I don't find I nice example for categories, so let me to switch
| to another example.
| 
| define Cat: Category == with;
| define Ying: Category == with {
|   1: %
|   foo: (%, %) -> %;
| }
| Dom(D: Cat): Ying == add {
|   Rep == Integer;
|   import from Rep;
|   1: % == per(1$Rep);
|   foo(x:%, y:%):% == per(rep x + rep y);
| }
| DI: Cat == Dom(Integer) add;
| DS: Cat == Dom(String)  add;
| DJ: Cat == Dom(Integer) add;
| 
| DI, DJ, and DS are 3 different domains (because of the "add").
| (Which means the compiler should forbid
| 
|   (foo$DI)(1$DJ, 1$DJ)

OK.

| You probably would like
| 
|   (foo$DI)(1$DI, 1$DI)
| 
| to work.

OK.

| What about
| 
|   (foo$Dom(Integer))(1$Dom(Integer), 1$Dom(Integer))
| 
| ?

I would like it to work too.

| You agree that the "add" part of Dom(Integer) and Dom(String) are identical
| (in source code). (So many different equality meanings, its hard to tell
| somebody else what I actually mean.)
| 
| I probably should not be able to call
| 
|   (foo$Dom(Integer))(1$Dom(String), 1$Dom(String))
| 
| right?

Yes.

| But allowing
| 
|   (foo$Dom(Integer))(1$Dom(Integer), 1$Dom(Integer))
| 
| and forbidding
| 
|   (foo$Dom(Integer))(1$Dom(String), 1$Dom(String))
| 
| can only be done if you have a functional language when it comes to types.

Surely, a functional type system will ease that.  But is it necessary?
I'm not saying we should have a non-functional type system; I'm curious
as of the logical  implications one way or the other.

| Dom(Integer) should be the same as Dom(Integer) in
| 
|   (foo$Dom(Integer))(1$Dom(Integer), 1$Dom(Integer))
| 
| otherwise that does not typecheck.

Yes.  That works within Dreyer's framework, I think.

[...]

| In case of Foo(Integer) and Foo(String) there would be no (implemented) "="
| anyway. We cannot compare domains and cannot compare categories. All we could
| do is to use "pretend" and compare pointers. But uhhhhh..... nobody wants
| that.

Right -- I don't want pretend and pointer comparion that way :-)
At least not in "everyday programs".

-- Gaby