On Fri, Jul 4, 2008 at 2:18 PM, Gabriel Dos Reis wrote: > Bill Page writes: > > | On Fri, Jul 4, 2008 at 7:40 AM, Gabriel Dos Reis wrote: > | > Bill Page writes: > | > > | > | On Thu, Jul 3, 2008 at 12:18 PM, Gabriel Dos Reis wrote: > | > > | > | There is a related problem with the definition of the domain > | > | 'Category' - is it a domain or a category? > | > > | > Category is conceptually a category, just like Domain is conceptually > | > a category. > | > | What do you mean by "conceptually a category"? As far as I can see > | Domain is a domain - not conceptually a category at all. > > Why? >
Simply because I can write: x:Domain := Domain The only category I can see associated with Domain is called Type in OpenAxiom. By "conceptually a category" do you just mean that Domain is conceptually the same as Type? > ... > | > | To me the phrase: "... the *domain* Type" (my emphasis **) says > | specifically that Type is a domain. How else can I understand it? > > OK, let me rephrase my question. We are trying to understanding > why `Type' *must* be a domian (your position). No. I am only pointing out that Type is a domain in Aldor. I did not claim that this necessary. My claim however *is* that Domain in OpenAxiom plays the same role as Type in Aldor and that in OpenAxiom Domain is a domain. I admit that in OpenAxiom Type might usefully be defined as a category. In that case it does not make sense to write x:Type := ... but that is ok because all we need is x:Domain := ... | > | I think the way out of this mess was correctly identified by Stephen | > | Watt in the description of Aldor when he wrote: (ibid.): | > | | > | "Each domain is itself a value belonging to the domain Type. Domains | > | may additionally belong to some number of subtypes (of Type), known | > | as categories." > ... > Nothing in the semantics specification (the quote above without the > first sentence) requires Type to be a domain. > I agree. > ... > Could you supply an executable semantics for the plain English > quote? > I am not clear on exactly what you mean by "executable semantics", but to do that probably requires a definition of subtype. I am sure you are aware that the details (for Aldor) are provided in the Aldor Users Guide, but here all we need is an understanding of categories as forming a lattice (complete partial order) or inclusion relation given by 'Join' and 'with', having Type as it's least element. For example compiling: X():Category == Join(Y,Z) and A():X == add ... defines A as belonging to X, Y, Z and Type. > ... > | > | > The decision to make Type a domain is a separate one. > | > | If I want to be able to write: > | > | x:Type := ... > | > | then it seems very clear that Type must be a domain. > > If it is so very clear to you, then you must be able to explain > the reasons so very simply. > The only values in Axiom (and Aldor) are objects of some domain. > Why is it so fundamental that Type must be a domain, and that > reason does not carry to Ring? After all, why can't one write > > y: Ring := Integer > > ? In Aldor that is ok. The fact that Type is a domain does carry over to Ring. In OpenAxiom Type is a category so that status of Ring as a type is less clear. However in a separate email I did make a proposal for what it might stand for in this context. > ... > So, if you could write > > x: Ring := ... > > Would Ring cease to be a category? > No. > ... Regards, Bill Page. ------------------------------------------------------------------------- Sponsored by: SourceForge.net Community Choice Awards: VOTE NOW! Studies have shown that voting for your favorite open source project, along with a healthy diet, reduces your potential for chronic lameness and boredom. Vote Now at http://www.sourceforge.net/community/cca08 _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
