[Aldor-l] [open-axiom-devel] [#428] 'Domain' in 'SetCategory'?

Bill Page bill.page at newsynthesis.org
Thu Jul 3 22:47:55 EDT 2008


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. Usually these also
correspond to some recognizable "category" in the mathematical sense,
e.g. Ring. But what concept is represented by the category Type? (A
possible answer is provided by Saul Yousseph, but I do not think that
was the original intention of the design of Axiom.)

There is a related problem with the definition of the domain
'Category' - is it a domain or a category?

Earler in this thread I gave the example:

(3) -> x := IntegerNumberSystem

  (3)  IntegerNumberSystem
                                                    Type: Category

but this fails:

(4) -> x:Category := IntegerNumberSystem

  Category is a category, not a domain, and declarations require
     domains.

and one can also write:

(4) -> Integer has Category

  (4)  true
                                               Type: Boolean

But we find:

(5) -> I:Type := IntegerNumberSystem

   Type is a category, not a domain, and declarations require domains.

(5) -> I:Domain := IntegerNumberSystem

   (5)  IntegerNumberSystem
                                                Type: Category


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

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

-----------

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

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.

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

'Domain' is a domain, but are sub-domains of domain also domains? So
again, what is Category?

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

I guess I am still a little confused about all of this. :-)

Regards,
Bill Page.



More information about the Aldor-l mailing list