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

Reply via email to