login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

Edit detail for Rep and Per revision 1 of 2

1 2
Editor:
Time: 2007/11/24 21:42:24 GMT-8
Note:

changed:
-
Aldor programming philosophy from the point of view of it's
evolution from previous incarnations of the Axiom library
compiler, is described here:

http://www.aldor.org/docs/HTML/chap18.html

There is one construct in particular in Aldor that really
stands out - the concept of representation and it's opposite
(abstraction?). In Aldor these are formally denoted
by two very peculiar coercion operations: 'rep' and 'per'.

In older SPAD terms, rep and per can be written as the following
macros::

  macro {
        rep x == x @ % pretend Rep;
        per r == r @ Rep pretend %;
  )

The expression 'rep(x)' describes an object x of this domain but
treats it as belonging to a different domain 'Rep'.

The expression 'per(y)' describes an object y from the 'Rep' domain
which is to be treated as belonging to this domain. ('per' as in
the percent % symbol)

In looking through older SPAD code it is clear that these
combinations occur frequently and their encapsulation as 'rep'
and 'per' makes reading Aldor code much easier than SPAD.

Does anyone know of any formal programming language research
papers that describe the semantics of 'rep' and 'per' in a
general way? If this sort of mechanism is present in other
languages, what form does it take?

It seems to me that 'rep' and 'per' constitute the essence of the
peculiar object-oriented programming style pioneered by Axiom
and Aldor. But what are these constructs in formal (categorical)
terms?

Below is a first attempts to answer these questions -
comments, corrections and opinions would be most welcome!

<hr />

It seems appropriate to me to think of rep and per as forming
a pair of adjoint functors::

             rep
            ---->
   % domain       Rep domain
            <----
             per

'rep' is a "forgetful functor" that maps the abstract structure
(objects and operations) of this domain into it's internal
representation. It "forgets" about the abstract relationships.
The objects of the external domain however are viewed only in
terms of the relationships between objects. The image of this
domain under 'rep' in representation has its internal structure
exposed.

'per' on the other hand constructs abstract members of this
domain from the underlying representation. It encapsulates
the internal operations of the representation in terms of
the abstract structure of this domain.

domains must be thought of in terms of categories both in the
sense of category theory and in Axiom's sense of "category".
The appropriate categories usually have at least the structure
of a Cartesian closed category which they inherit from
Axiom's basic types constructors, record, union and mapping.
See discussion:
http://wiki.axiom-developer.org/TuplesProductsAndRecords

In terms of category theory there is a natural transformation,
called the 'unit', that partitions elements of the Rep domain
into classes (as an abstract quotient of the representation)::

  x --> rep(per(x))

and 'rep' is right adjoint of 'per'.

In category theoretic terms 'Rep' domain is some Cartesian closed
category, i.e. consisting of products (records), co-products
(unions) and exponentials (functions) over some basic set
of component domains. It's operations are formed freely from
the operations of it's components.

The implementation of the domain in terms of the representation
establishes a natural bi-jection between the operation of the
external domain and the operation of it's internal representation::

   x -> rep y    (representation)
  ------------
   per x -> y    (domain)

The book: "Basic Category Theory for Computer Scientists", by
Benjamin Pierce, MIT Press, 1991, is a good reference. See
especially section 2.4. Pierce gives an excellent example in
terms of definition of the 'List' constructor.

Also: "Categories, Types and Structures. An introduction to Category
Theory for the working computer scientist." by Andrea Asperti and
Giuseppe Longo, M.I.T. Press, 1991, which is downloadable from here:
http://www.di.ens.fr/users/longo/download.html

Regards,

Bill Page.

*(from an email to axiom-develper on Thursday, September 01, 2005 6:36 AM)*



Aldor programming philosophy from the point of view of it's evolution from previous incarnations of the Axiom library compiler, is described here:

http://www.aldor.org/docs/HTML/chap18.html

There is one construct in particular in Aldor that really stands out - the concept of representation and it's opposite (abstraction?). In Aldor these are formally denoted by two very peculiar coercion operations: rep and per.

In older SPAD terms, rep and per can be written as the following macros:

  macro {
        rep x == x @ % pretend Rep;
        per r == r @ Rep pretend %;
  )

The expression rep(x) describes an object x of this domain but treats it as belonging to a different domain Rep.

The expression per(y) describes an object y from the Rep domain which is to be treated as belonging to this domain. (per as in the percent % symbol)

In looking through older SPAD code it is clear that these combinations occur frequently and their encapsulation as rep and per makes reading Aldor code much easier than SPAD.

Does anyone know of any formal programming language research papers that describe the semantics of rep and per in a general way? If this sort of mechanism is present in other languages, what form does it take?

It seems to me that rep and per constitute the essence of the peculiar object-oriented programming style pioneered by Axiom and Aldor. But what are these constructs in formal (categorical) terms?

Below is a first attempts to answer these questions - comments, corrections and opinions would be most welcome!


It seems appropriate to me to think of rep and per as forming a pair of adjoint functors:

             rep
            ---->
   % domain       Rep domain
            <----
             per

rep is a "forgetful functor" that maps the abstract structure (objects and operations) of this domain into it's internal representation. It "forgets" about the abstract relationships. The objects of the external domain however are viewed only in terms of the relationships between objects. The image of this domain under rep in representation has its internal structure exposed.

per on the other hand constructs abstract members of this domain from the underlying representation. It encapsulates the internal operations of the representation in terms of the abstract structure of this domain.

domains must be thought of in terms of categories both in the sense of category theory and in Axiom's sense of "category". The appropriate categories usually have at least the structure of a Cartesian closed category which they inherit from Axiom's basic types constructors, record, union and mapping. See discussion: http://wiki.axiom-developer.org/TuplesProductsAndRecords

In terms of category theory there is a natural transformation, called the unit, that partitions elements of the Rep domain into classes (as an abstract quotient of the representation):

  x --> rep(per(x))

and rep is right adjoint of per.

In category theoretic terms Rep domain is some Cartesian closed category, i.e. consisting of products (records), co-products (unions) and exponentials (functions) over some basic set of component domains. It's operations are formed freely from the operations of it's components.

The implementation of the domain in terms of the representation establishes a natural bi-jection between the operation of the external domain and the operation of it's internal representation:

   x -> rep y    (representation)
  ------------
   per x -> y    (domain)

The book: "Basic Category Theory for Computer Scientists", by Benjamin Pierce, MIT Press, 1991, is a good reference. See especially section 2.4. Pierce gives an excellent example in terms of definition of the List constructor.

Also: "Categories, Types and Structures. An introduction to Category Theory for the working computer scientist." by Andrea Asperti and Giuseppe Longo, M.I.T. Press, 1991, which is downloadable from here: http://www.di.ens.fr/users/longo/download.html

Regards,

Bill Page.

(from an email to axiom-develper on Thursday, September 01, 2005 6:36 AM)