On Fri, Jul 4, 2008 at 2:18 PM, Gabriel Dos Reis wrote: > ... > Bill Page writes: > | I agree that just giving Type a domain definition is not a solution. I > | think the solution to the problem has to do with defining more > | precisely what is a "category" (i.e. in the case of Aldor a categories > | are subtypes of Type, domains are objects of Type and therefore via > | the subtype relation domains are also objects of categories). > > Depending on ones notion of `subtype', it is already the case that > a category is a subtype of Type -- if by x is subtype of Type one > means that the query > > x has Type > > is well formed and yields true.
But Integer has Type is well-formed and yields true. Does that mean that Integer is a subtype of Type, i.e. a category? Of course not! Axiom has two different uses of 'has'. One of them represents the subtype (inclusion) relation, the other is the membership relation. > ... > | (4) -> w:Domain:=Category > | > | (4) Category > | Type: Type > | -------- > | > | I think that 'Type: Type' does not make sense > > Why? > ... In OpenAxiom Type is a category. By 'w:Domain' we just declared that 'w' is a variable taking values from Domain but it's type is given as Type. Surely just as we declared, it's type must still be Domain. No? > > In the base AXIOM system and in FriCAS I do not recall seeing Domain > as being defined as a domain -- in fact, it has no definition at all. > That is (almost) correct. There is no definition in the Axiom library - you corrected that and the same solution could be applied in Axiom. (In fact I experimented with something like this a few years ago.) But the Axiom interpreter does generate such names apparently in the expectation that these should be defined somewhere. Apparently this was some development that was only partially implemented or perhaps code rot removed these infrequently used parts at some point in the evolution of the system. > ... > OpenAxiom's take is that to bridge the gap between the two level, > one would really on satisfaction of properties defined through the > `has' operator. > So can you define very clearly the properties of 'has' in OpenAxiom? As an operator does it have a definable signature? If so is it polymorphic, having more than one form? 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
