On Fri, Jul 4, 2008 at 7:40 AM, Gabriel Dos Reis wrote:
> Bill Page writes:
>
> | On Thu, Jul 3, 2008 at 12:18 PM, Gabriel Dos Reis wrote:
> | > ...
> | > The fact that `Type' is a category, but not a domain is something
> | > that OpenAxiom inherits from 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 problems e.g. in the case of Aggregate.
>
Although Type is a domain in Aldor, exactly this sort of construction
is used there without a problem (notwithstanding a separate issue
raised by Ralf concerning the use of 'has' in Aldor). Why do you think
it is a problem in SPAD?
> [...]
>
> | 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.
What do you mean by "conceptually a category"? As far as I can see
Domain is a domain - not conceptually a category at all.
> 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.
Yes, this is clear. A representation of categories and domains as
values (objects) is definitely required. As I understand it, in Axiom
objects belong only to domains. So categories and domains must be
domains.
> Therefore Category and Domain do have domain definition, but they
> are conceptually categories.
>
I think that before we can make sense of what it means to be
"conceptually a category" it is necessary to first define
unambiguously what is a "category". Stephen Watt defined it as I
quoted below:
>
> | 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 flavors of AXIOM, I think.
>
That is not clear to me. I think at best this might be implemented in
different flavors of Axiom in different ways and in a more or less
consistent manner.
> | 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.
To me the phrase: "... the *domain* Type" (my emphasis **) says
specifically that Type is a domain. How else can I understand it?
> All it says is a semantics requirement on the value of
>
> x has Type
>
> for all domains x.
>
The quotation from Stephen Watt makes no reference to 'has'. 'has' is
defined elsewhere in the Aldor documentation under the subject of type
satisfaction. In both Aldor and Axiom the thing to the right of 'has'
must be a category, so in Aldor it is not possible to write:
x has Type
because Type is a domain - not a category.
> The decision to make Type a domain is a separate one.
If I want to be able to write:
x:Type := ...
then it seems very clear that Type must be a domain. That is what is
done in Aldor. But I agree that it may be possible to find another
solution. In particular in OpenAxiom you have introduced a new domain
called Domain that plays a similar role to Type in Aldor. That allows
you to retain then name 'Type' for something else - a category. I
proposed in my previous message that what it turns out to be is just
Domain considered as a subdomain of itself. As far as I know Aldor has
no name for this although Stephen Watt's definition would apparently
allow it, i.e. the subtype of Type consisting of exactly all of Type.
> One I have considered many times in the past, mostly when I
> decided to give Domain and Category definitions.
Yes I understand. I would argue similarly that writing in OpenAxiom
x:Domain := ...
x:Category := ...
implies that Domain and Category are domains. However the following of
course are all errors of various kinds:
x:Type := 1
x:Domain := 1
x:Domain := IntegerNumberSystem
x:Category := 1
x:Category := Integer
> 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.
>
I agree that just giving Type a domain definition is not a solution. I
think the solution to the problem has to do with defining more
precisely what is a "category" (i.e. in the case of Aldor a categories
are subtypes of Type, domains are objects of Type and therefore via
the subtype relation domains are also objects of categories).
That Type and subtypes of Type (categories) are also domains is not a
central part of the resolution of the problem but rather more a matter
of convenience. It means that this "two-level system" is essentially
flat.
> |
> | 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'
>
> ?
That is a key part of the definition give by Stephen Watt:
"... subtypes (of Type), known as categories."
Unlike OpenAxiom, Aldor does not define 'Domain' as a domain, but
'Type' is literally a domain. Domains are all objects of a
distinquished domain called 'Type'. (Quote: "Each domain is itself a
value belonging to the domain Type."). As I see it, OpenAxiom has used
the name 'Domain' in the same way that Aldor used the name 'Type'. So
in OpenAxiom we may write:
x:Domain := Domain
but in Aldor we would say:
x:Type := Type;
So finally in OpenAxiom we should say:
"Categories are sub-domains of 'Domain."
The most recent revision of Open-Axiom gives these results:
(1) -> x:Domain:=Domain
(1) Domain
Type: Type
(2) -> y:Category:=IntegerNumberSystem
Category is a category, not a domain, and declarations require
domains.
(2) -> y:Domain:=IntegerNumberSystem
(2) IntegerNumberSystem
Type: Category
(3) -> z:Domain:=Integer
(3) Integer
Type: Domain
(4) -> w:=Domain:=Category
You have used the abbreviation Domain of the constructor Domain on
the left-hand side of an assignment expression. This is not
allowed.
(4) -> w:Domain:=Category
(4) Category
Type: Type
--------
I think that 'Type: Type' does not make sense and (2) and (4) above
should not be errors.
>
> | 'Domain' is a domain, but are sub-domains of domain also domains?
>
> Exactly what do you mean by this?
>
Stephen Watt's definition does not require that sub-types of Type are
domains - only that Type itself is a domain. However in Aldor (and
Axiom) we also want categories to be values (object) belonging to some
domain called Category.
> | So again, what is Category?
>
> See my answer above. It is the type of all category objects.
I think that is ok provided Category is itself a domain. But it misses
an important aspect: Objects of type Category are subtypes of Type
(subdomains of Domain).
>
> | 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 am guessing and trying to fill-in the blanks since as far as I know
there is no written documentation in Axiom about this, but it seems to
me that SubDomain must be a domain constructor that takes a domain as
argument. Specify we need
Category = SubDomain(Domain)
But Domain is itself a domain so maybe one should be able to write, for example:
x:SubDomain(Integer) := PositiveInteger
??
> | 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.
>
Ok, I agree. I think that is exactly what Stephen Watt's definition
accomplishes by: "Domains are objects of the domain Type and
Categories are subtypes of Type". The difference between the two
levels is one of membership versus subsets.
> ...
Regards,
Bill Page.
-------------------------------------------------------------------------
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
