There seems to be different understandings of Type, domain, category, Category, etc. around.
Here is an attempt to collect all these different opinions in order to make discussion about them
clearer.
Some related referemces in the email list archives:
Definitions of Ralf Hemmecke
A category is an L-type whose type is the language-defined constant Category.
A domain is an L-type whose type is a category.
An L-type is either a category, a domain or the language-defined constants Category and Type.
Any L-type is of type Type.
I wrote L-type to mean type in the language, either Aldor or SPAD.
In
- Stephen Watt wrote:
- The type system has two levels: Each value belongs to some unique type,
known as its domain, and the domains of expressions can be inferred statically.
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.
Categories can specify properties of domains such as which operations they export,
and are used to specify interfaces and inheritance hierarchies.
-
- The biggest difference between the two-level domain/category model and the
single-level subclass/class model is that a domain is an element of a category,
whereas a subclass is a subset of a class. This difference eliminates a number of
problems in the definition of functions with multiple related arguments.
In
Section 7.2 of the AUG is written:
- A domain is a type which defines a collection of exported symbols. The
symbols may denote types, constants and functions. Many domains also
define an interpretation for data values, called a representation type; these
domains are also known as abstract data types. Those domains which are
not abstract datatypes are called packages.
- A category is a type which specifies information about domains, including
the specification of the public interface to a domain, which consists of
a collection of declarations for those operations which may be used by
clients of the domain.
That conflicts the above statement that Type is a domain, but is in line with the
two-level domain/category model.
See also Sections 7.8 (Domains) and
7.9 (Categories) of the Aldor User Guide.
I haven't (yet) found a sentence that says that Type or Category are domains.
Section 7.5 Subtypes
Every value in Aldor is a member of a unique domain which determines the interpretation of its data.
Section 7.9 Categories
All type values have ``Type'' as their unique base type. As with all other values, it is the unique base type which determines how values are to be represented.
The language allows categories to be treated as normal values and allows names to refer to categories. A category (by definition) is a value of the Aldor built-in type Category.
I have nothing against
Type being a type. But
Type is not an Aldor-domain.
Maybe it is a domain in a broader sense, but that sense is only vaguely defined, if at all.
I would like not to use
domain and
type interchangeably.
The fact that
Type is a domain certainly does not make domain
and type interchangeable. Objects of the domain
Type are
themselves either domains
or categories, so type and domain
are still not interchangeable since categories are not domains.
Could you explain why you claim that "Type is not an Aldor-domain".
Is this only a personal preference? To me: "If it talks like a duck
and it looks like a duck, its a duck...". In this case the compiler
output, the library definitions, and quotations from the primary
developer all agree:
Type has with {};
returns true.
I simply have not found an explicit statement in the AUG that says that
Type and
Category are domains. How else could I claim that they are?
And regardless of what others say, could you give your definitions similar
to what I started at the beginning of this page? Let's first collect the status,
before we argue, what implications it would have if Type would be a domain.
Maybe in the end it doesn't matter whether or not Category and Type are domains.
Actually I sort of agree. From a formal perspective it seems rather
surprising to me that it is possible to have done so much (good!)
programming in Axiom and Aldor yet nevery having fully resolved
such fundamental issues. Probably it has more impact on internal
aspects of the compiler and interpreter than it does for most users.
But I think some styles of programming - for example the kind used
for the
species project
- might benefit from a clear definition and a reliable implementation.
Personally I think Aldor is a brilliant distillation and
crystallization of the concepts that evolved from SPAD in Axiom.
It's novel "categorical" alternative to the class/subclass concepts
of the object-oriented paradigm is probably still under-appreciated
by language designers. The discipline of programming language
design in the meantime has largely moved on to other issues but
this tradition can be carried on in Axiom by the OpenAxiom project.
Definitions by Bill Page
This is a first draft in point form of how I think domains and
categories should work in at least OpenAxiom:
- Domains implement all data and algebraic structures in OpenAxiom.
SPAD and the OpenAxiom interpreter build-in only the minimum
bootstrap data structures necessary to compile and access domains
from the Axiom library.
- All values are values in some domain that defines all of the
operations that can be performed on these values. In general
these values are created and accessible at run-time data except
as noted below.
E.g.:
a:A := new()$A
declares a as a variable with values in domain A returned by
an operation called new in A.
- Domains themselves are values of the domain Domain and as
such are also treated as run-time accessible data (first-order).
Domains are created at compile-time and stored in the Axiom
library. At the present there are no operations that create new
domains at run-time but domains can be passed and returned as
values.
E.g.:
d:Domain := A
declares d as a variable whose value is the domain A. The
domain Domain provides some additional reflective and
syntactical operations on domains such as equality.
E.g.:
(d = A)@Boolean
is true only if d has the value A.
- Categories are subdomains of Domain specified by both name
and a list of exported operations.
E.g.:
X:Category == with
f: A -> B
By "subdomain" is meant that the domains in Domain are also
values in some category only if they reference that category by
name and implement the required exported operations.
E.g.:
D:X == add
f(x) == ...
As subdomains of Domain, categories are themselves domains and
can be used in declarations of variables and parameters.
E.g.:
a:X := A
#:X->Integer
Categories are organized into a lattice by referring to other
categories by name.
E.g.:
Y:Category == X with
g: B -> A
or:
Z:Category == Join(X,Y)
The list of exported operations is the union of all exported
operations of the categories to which it refers plus those
give after with.
- Categories are values of the domain Category and as such
are also treated as run-time accessible data (first-order).
Category is itself a value of Domain. Like domains,
categories are created at compile-time and stored in the
Axiom library. There are currently no operations that create
new categories at run-time but categories may be passed and
returned as values. The domain Category provides some
additional reflective and syntactical operations on categories
such as
= and has. E.g.:
has:(Union(Category,Domain),Category) -> Boolean
A has X
is true if A refers to X or to a category that refers to X
applied recursively.
- Type is the category in Category consisting of all
domains in Domain. All categories are subcategories of
Type. Type does not export any operations.
On Tue, Jul 8, 2008 at 3:06 PM Gabriel Dos Reis wrote:
I'll be using the word specification in an informal sense that I
hope is clear from context.
A category is a collection of specifications. A domain is a
collection of implementations. An object is any computational
values in an OpenAxiom program. An object has a representation given
by a domain. An object O is said to have type d if d implements
the reprsentation for the object O.
A category constructor is a category-valued function, defined with
the term Category as its return type.
A domain constructor is a domain-valued function, defined with a
category as its return type.
Category contructors and domain constructors may be parameterized by
domains and categories. Furthermore, domains and categories have
runtime representations, e.g. they are reflected as objects in
OpenAxiom. In particular, domains objects have type Domain, and
category objects have type Category. And Domain and Category
are indeed domains, because they implement specifications and provide
object representations.
I did not discuss the notion of package, as it is almost like
a domain - it implements specifications - except that it does not
provide object representation.
-- Gaby