[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