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
-------------------------------------------------------------------------
Check out the new SourceForge.net Marketplace.
It's the best place to buy or sell services for
just about anything Open Source.
http://sourceforge.net/services/buy/index.php
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
