Re: [open-axiom-devel] [#428] 'Domain' in 'SetCategory'?

[Bill P. <bil...@ne...>]

On Wed, Jun 18, 2008 at 3:15 AM, Ralf Hemmecke wrote:
> ...
> I must admit that I like the idea of Saul Youssef
> http://physics.bu.edu/~youssef/homepage/talks/categories/21.html
>
> Domain: Category == with;
>
> An object X: Domain would be called a "domain" that is similar
> to C: Category where we call C a category (in the Aldor sense).
>

But in this case unless we assert it, not every domain has Domain.
Declaring X:Domain or X:Domain with ..., or X:Join(Domain, ...) is
just making this assertion. It does not provide X with the
characteristics of an "object", which by definition is an instance of
some domain.

That category that plays this role in Axiom is called Type

(1) -> )sh Type
 Type  is a category constructor
 Abbreviation for Type is TYPE
 This constructor is exposed in this frame.
 Issue )edit /usr/local/lib/open-axiom/i386-pc-solaris2.10/1.2.0-2008-05-28/src/algebra/TYPE.spad
to see algebra source code for TYPE

------------------------------- Operations --------------------------------
                          No exported operations

When treated as values, all domains and categories must belong to some
domain that provides as a minimum at least a coercion of these values
to OutputForm. E.g.

(1) -> x:=SetCategory

   (1)  SetCategory
                                                      Type: Category
(2) -> y:=Integer

   (2)  Integer
                                                      Type: Domain

(3) -> )show Category
 Category  is a domain constructor
 Abbreviation for Category is CATEGORY
 This constructor is not exposed in this frame.
 Issue )edit /usr/local/lib/open-axiom/i386-pc-solaris2.10/1.2.0-2008-05-28/src/algebra/CATEGORY.spad
to see algebra source code for CATEGORY

------------------------------- Operations --------------------------------
 coerce : % -> OutputForm

(3) -> Category has Type

   (3)  true
                                              Type: Boolean

(4) -> )sh Domain
 Domain  is a domain constructor
 Abbreviation for Domain is DOMAIN
 This constructor is not exposed in this frame.
 Issue )edit /usr/local/lib/open-axiom/i386-pc-solaris2.10/1.2.0-2008-05-28/src/algebra/DOMAIN.spad
to see algebra source code for DOMAIN

------------------------------- Operations --------------------------------
 coerce : % -> OutputForm              reflect : ConstructorCall -> %
 reify : % -> ConstructorCall          showSummary : % -> Void

(4) -> Domain has Type

   (4)  true
                                                                Type: Boolean

I think that what Saul is saying about Domain can be applied to Type.
The idea is that Type can be viewed as a mathematical category whose
objects (in the categorical sense) are domains and whose morphisms are
Axiom functions. We get Product, Union and Exponentiation for free. I
think it makes sense to claim that Axiom also provides a Natural
Numbers Object (e.g. PositiveInteger) and sub-objects (subdomain and
Boolean), although their connection to category theory is not so well
developed. So a strengthened form of Saul's thesis would be that Type
is a Topos.

But the structure of Type is quite different than the structure of a domain.

> Oooops, now I see that Gaby has also written in domain.spad.pamphlet:
>
> Category(): Public == Private where
>   Public ==> CoercibleTo OutputForm
>   Private ==> add
>     coerce x ==
>       outputDomainConstructor(x)$Lisp
>
> Isn't "Category" part of the SPAD language? I am a bit confused
> and unfortunately the documentation in that file does not help me
> out. There is at least a reference to "further reading" missing.
>

Yes. Category is the domain of categories, i.e. categories as values.
Category constructors create these values. Operations like 'Join' and
'with' also construct new categories from old categories thereby
defining the category lattice. Type is the top category in this
lattice.

> What I see in syntax.spad.pamphlet all looks like adding reflection
> to SPAD. Is that the intention? Anyway I find
>
> Category(): Public == Private where ...
>
> somewhat confusing without any proper explanation of why it can and
> should be done this way.
>

Since we want to treat all Types as first-order objects I do not see
any other possibilities.

The only extension of this that I can imagine is to allow "domain
comprehension". By that I mean that we could also treat categories as
subdomains of Domain. Then writing

  X:C := D

where C is a category, could denote those domains that satisfy C

  Union(d for d in Domain | d has C)

E.g.

  X:IntegerNumberSystem := Romain

but right now this still returns an error

(5) -> X:IntegerNumberSystem:=Roman

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

Regards,
Bill Page.b