Re: [Axiom-developer] Unions in Spad

[Bill Page]

On 08 Jul 2007 22:27:00 -0400, Stephen Wilson wrote:
> ...
> "Bill Page" <address@hidden> writes:
> > But really I think the concept of "selectors" in both Union and Record
> > is at best a legacy of earlier days in programming language design. It
> > makes much for sense to me to define Union and Record as co-limit and
> > limit in the sense of category theory. Then Union selectors are just
> > injections operations and Record selectors are projection operations
> > which are exported like any other function from these types. There is
> > no need for any lower level language construct.
>
> Its been a while since I brushed up on Category Theory.  Yet another
> todo item.  I thought that limit and co-limit were defined w.r.t an
> index category.

Category theory is a BIG subject so unless you are motived in a more
general manner I would recommend that you focus on the more recent use
of category theory in computer science. Although there are several
others to choose from, I think one very good place to start or to
review is the following book by Benjamin Pierce:

@BOOK{PIERCE91,
 author = {Benjamin C. Pierce},
 title = {Basic Category Theory for Computer Scientists},
 year = {1991},
 publisher = {MIT Press},
 fullisbn = {0-262-66071-7},
 orderinginfo = {MIT PRESS 55 Hayward ST. Cambridge Mass 02142 USA
                 800-356-0343},
 europeinfo = {14 Bloomsbury Square London WC1A 2LP U.K. Facsimile:
                 071-404-0601},
 plclub = {Yes},
 bcp = {Yes},
 keys = {books}
}

You might also be interested in some of his papers on "Intersection
and Union Types". See his website at:

http://www.cis.upenn.edu/~bcpierce/papers/index.shtml

Limits and co-limits are defined in a very general manner as type of
universal construction. For a very quick and mostly adequate
introduction see:

http://en.wikipedia.org/wiki/Limit_(category_theory)

> How does this differ from the notion that an instance
> of Enumeration type serves as the index into a record or union, and
> how do the morphisms from the objects of the index category to the
> objects of the category representing the elements of a union/record
> differ from normal "selectors"?

The notion of product and co-product that is most relevant is found in
the category SET. But I think it is easy to argue that a category with
much less structure is a better starting point for the goals of Axiom
and a language like SPAD.

> Im probably missing some details, but
> from my modest understanding of Category Theory, I feel the
> categorical treatment is just a different vernacular to express the
> same thing.  There are undoubtedly generalizations Im missing, but I
> am curious how they might be expressed meaningfully in a programming
> language.

I agree that very often category theory (as currently used in computer
science) is "just a different vernacular to express the same thing" as
can be expressed in other more conventional ways. But the advantage
that I see in the categorical language is the very high level of
abstraction.

> Perhaps an example of how you envision this foundation working in
> Spad?

The Record type should export operations that correspond to what would
otherwise be called selectors, e.g.

Record(A:Integer, B:String)

should export

 A: % -> Integer
 B: % -> String

inaddition to the uniquely defined higher-order operation

 product: (A:Type, A->X,A->Y) -> (A->%)

arising from categorical universality.

See the example at:

http://wiki.axiom-developer.org/SandBoxLimitsAndColimits

Similarly

Union(A:Integer, B:Integer)

should export

 A: Integer -> %
 B: String -> %
 sum: (A:Type, X->A,Y->A) -> (% -> A)

Regards,
Bill Page.