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 _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer