"Bill Page" <[EMAIL PROTECTED]> writes: | On Fri, Jul 4, 2008 at 2:28 PM, Gabriel Dos Reis wrote: | > Bill Page writes: | > | | > | Yes, I proposed esentially this in a previous message. Well, not | > | that Ring *is* a domain but rather that through a principle of | > | "comprehension" (the term as used in set theory) Ring might stand | > | in this context as representing the domain | > | | > | Union(x for x in Domain where x has Ring) | > | | > | Such a domain embodies the concept of a category as a subdomain | > | of Domain. | > | > I hope Ring does not cease to be a category. | > | | Ring is still a category.
So, in your scheme something can be both a domain and a category. Is that right? | > From my perspective, if I have a function | > | > f(x:T): U == ... | > | > and I can name the parameters, then I should be able to declare | > variables of T too. This is the `first class value' principle used | > in programming languages. What we currently have is that the | > principle is not followed throughout. | | Agreed. | | > It is not clear to me that principle should force categories to | > become domains. You seem to argue that is `very clear', but | > you do not clear reasons. | > | | I do not think that it is necessary to force categories to become | domains but it makes sense to me that they be objects of the domain | Category. Evaluation of category forms already yields objects of the domain Category -- at least in OpenAxiom. | In the case that T in 'f(x:T): U == ... ' is a category I | have proposed that in this context T be interpreted as the domain | | Union(x for x in Domain where x has T) I do not fully understand why this (1) is computationally effective solution, (2) solves all the issues, (3) is better laternative. Would you mind exploring each of those points? | > From my perspective, categories are specifications and domains are | > implementations of specifications. Categories have no executable | > content, domains have executable contents: They implement | > specifications. | > | | I agree. But in any given situation is seems possible to "comprehend" | that the members of this Union all implement the same T so see no | problem with defining variables of T in this manner also. That assumes this `comprehension' is computationally effective. Which is not at all obvious to me. -- 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
