"Bill Page" <[EMAIL PROTECTED]> writes:
| On Fri, Jul 4, 2008 at 1:07 PM, Gabriel Dos Reis wrote:
| > "Bill Page" <[EMAIL PROTECTED]> writes:
| >
| > | On Fri, Jul 4, 2008 at 7:40 AM, Gabriel Dos Reis wrote:
| > | > ...
| > | > 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?
| > | >
| > |
| > | Mapping (e.g. A->B) is clearly a domain constructor since we can
| > | write:
| > |
| > | x:A->B := ...
| > |
| > | A->B is the type of x.
| >
| > From my perspective, that is putting the cart before the cattle.
|
| Cart before the horse? :-)
|
| > It is not because you can write
| >
| > x:A->B := ...
| >
| > that makes Mapping a domain constructor. If you could write
| >
| > y: Ring := Integer
| >
| > would that make Ring a domain, as opposed to a category?
| >
|
| 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.
>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. 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.
>From my perspective, categories are specifications and domains are
implementations of specifications. Categories have no executable
content, domains have executable contents: They implement specifications.
-- 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
