"Bill Page" <[EMAIL PROTECTED]> writes: | Gaby, | | In a previous email you said you thought SubDomain was "half-baked".
Indeed. | If you meant this in the sense of "not fully implemented" then I agree Not just fully implemented, but also not fully specified, and in fact the semantics seems fuzzy (at best) once one starts using it. For example, the SubDomain constructor takes two arguments: The parent domain and the predicate that test whether to consider an object a member of the subdomain. Yet, you have use it with only one argument without specficifying what that would mean. | but if you meant that you think it was "ill-conceived" than I no | longer agree. I think that the type system of Axiom could be completed | that way. | | On Tue, Jul 8, 2008 at 9:26 PM, Gabriel Dos Reis wrote: | > Bill Page writes: | > | | > | Since 'Type' is the category of 'Domain', perhaps one should write: | > | | > | Type():Category == SetCategory with ... | > | | > | Domain():Type == add ... | > | | > | Then | > | | > | Category():Type with ... == SubDomain Domain | > | | > | In other words Category is a Domain with additional exports. | > | > I'm unclear about | > | > (1) Why Type should extend SetCategory; | | The bug report that (re-)started this topic was: | | http://axiom-wiki.newsynthesis.org/[EMAIL PROTECTED] | | In that page I observed that putting Domain in SetCategory provided a | solution to the problem. (Later you implemented this in a patch to | OpenAxiom.) | | But in | | http://axiom-wiki.newsynthesis.org/[EMAIL PROTECTED] | | I argued that Type is just Domain as a category and the OpenAxiom | interpret already returns: | | (1) -> Domain has Type | | (1) true | Type: Boolean I don't think this is evidence that Type is just Domain. In fact we have been through the argument that Type is a domain before and I do not remember we reached a definite conclusion. | | So having Type extend SetCategory and define Domain and Category in | terms of Type seemed to make sense. However I also wanted Type to be | the top of the category hierarchy (supremum of the lattice) so I guess | this is half-baked (ill-conceived). All we really need is Well, I do not understand why everything T satisfies T has Type should have an equality. That is my point. -- 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
