[ dropping Aldor list this is purely OpenAxiom discussion. ] "Bill Page" <[EMAIL PROTECTED]> writes:
| On Thu, Jul 3, 2008 at 12:18 PM, Gabriel Dos Reis wrote: | > ... | >> Bill Page wrote: | >> You are right, there is a difference between Aldor and OpenAxiom. | >> In Aldor Type is not a category - it is a domain! | > | > Yes. The fact that `Type' is a category, but not a domain is something | > that OpenAxiom inherits form the base AXIOM system. On many | > occasions I've found it a blessing and a curse. | > | | It is not clear to me when it might be a blessing... :-) As I see it, | the main purpose of a category in OpenAxiom is to stand for some | mathematical (or datastructure-like) concept. See the definition of the various collections. They have a heading like HomogeneousAggregate(S: Type): Category == ^^^^^^^ A most general category is needed here. The `magic' that is applied to Category and Domain could be applied to Type, but that would pose its own set of probems e.g. in the case of Aggregate. [...] | 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. Note that in the base AXIOM system, those don't have representations and that can prove problematic on more than one occasion. Categories and domains are objects; the ability to pass them around and return them as function values, requires that we have a representation for them. Therefore Category and Domain do have domain definition, but they are conceptually categories. [...] | > It is annoying when your realize that OpenAxiom can correctly | > evaluate [Ring, Integer] as a List Type, but will not be able to print | > it correctly. The reason being that Type is a category, therefore does | > not know (yet) how to print itself, | | Yes. As a category Type can have no exports. The problem isn't that it has no exports -- that is basically required for the most general category. The problem is that it is a category. | | > i.e. the query | > | > Type has CoercibleTo OutputForm | > | > is meaningless. | > | | Yes. But as I understand it, in Axiom (OpenAxiom?) 'has' has two meanings | | x has y | | is true if 1) domain 'x' satisfies category (or property) 'y' or 2) if | category 'x' is a subset of category 'y'. | | Under the second interpretation 'Type has x' is necessarily false for | any category 'x' not identical to 'Type'. Similarly, | | x has Type | | is necessarily true if it is defined at all. Yes. | 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." This is already the case of all flavours of AXIOM, I think. | I.e. 'Type' is a Domain. Categories are subtypes of Type, but as such | Type (being itself a subtype of Type) is also a category unless we | consider only proper subtypes. The quote you gave does not itself impose that Type must be a domain. All it says is a semantics requirement on the value of x has Type for all domains x. The decision to make Type a domain is a separate one. One I have considered many times in the past, mostly when I decided to give Domain and Category definitions. The fact that we have a two-level system implies that somewhere this kind of problem will surface again, so just giving Type a domain definition is not necessarily a solution to the fundamental problem. | | In OpenAxiom we now have the domain named 'Domain' so we should be | able to say: "Each domain is itself a value belonging to the domain | 'Domain'. Categories are sub-domains of 'Domain'. Then 'Type' is just | Domain as a whole considered as a category." Why *should* we be able to say that? Especialy, that # Categories are sub-domains of 'Domain' ? | 'Domain' is a domain, but are sub-domains of domain also domains? Exactly what do you mean by this? | So again, what is Category? See my answer above. It is the type of all category objects. | For example IntegerNumberSystem is a category. Right now OpenAxiom says: | | (1) -> I:=Integer | | (1) Integer | Type: Domain | | (2) -> x:=IntegerNumberSystem | | (2) IntegerNumberSystem | Type: Category | | But in FriCAS (and Axiom), we still get: | | (1) -> I:=Integer | | (1) Integer | Type: Domain | | (2) -> x:=IntegerNumberSystem | | (2) IntegerNumberSystem | Type: SubDomain Domain | | ------ | | which I guess is technically correct, unfortunately 'Domain' and | 'SubDomain' where never defined as domain constructors in either Axiom | or FriCAS. OpenAxiom corrected that problem but it introduced | 'Category' as a domain (sometimes) instead of defining 'SubDomain'. What is SubDomain? | I guess I am still a little confused about all of this. :-) The problem, as I see it, is fundamentally that of bridging the gap between two level systems. I would not like to add to the confusion, but when thinking of this problem one should also keep an eye on the status of Mapping. What is it? Is it a domain constructor or a category constructor? -- Gaby ------------------------------------------------------------------------- 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