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. > 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. 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) > > 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. 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
