[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] "has" and "with"
From: |
Gabriel Dos Reis |
Subject: |
Re: [Axiom-developer] "has" and "with" |
Date: |
Thu, 16 Aug 2007 11:43:23 -0500 (CDT) |
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
- Re: [Axiom-developer] "has" and "with", (continued)
- Re: [Axiom-developer] "has" and "with", Ralf Hemmecke, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Gabriel Dos Reis, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Ralf Hemmecke, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Gabriel Dos Reis, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Ralf Hemmecke, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Gabriel Dos Reis, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Ralf Hemmecke, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Gabriel Dos Reis, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Ralf Hemmecke, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Gabriel Dos Reis, 2007/08/16
- Message not available
- Re: [Axiom-developer] "has" and "with",
Gabriel Dos Reis <=
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), William Sit, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Bill Page, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Ralf Hemmecke, 2007/08/13
- Re: [Aldor-l] [Axiom-developer] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
- Re: [Aldor-l] [Axiom-developer] "has" and "with" (was curious algebra failure), Ralf Hemmecke, 2007/08/13
- RE: [Aldor-l] [Axiom-developer] "has" and "with" (was curious algebrafailure), Weiss, Juergen, 2007/08/13
- Re: [Aldor-l] [Axiom-developer] "has" and "with" (was curious algebra failure), Bill Page, 2007/08/13