[ 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
[email protected]
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
