Re: [Axiom-developer] Unions in Spad

[Stephen Wilson]

"Bill Page" <address@hidden> writes:

> 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)

OK.  Thanks for the suggestions!  Unsure when I will have time to
revisit this subject, but as I said, it is on my todo list.

[...]
> >
> > 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)

OK.  This is quite intelligible and perfectly reasonable.  I was
working with the assumption that you wanted a general mechanism to
express categorical concepts directly without recourse to builtin
primitives like Record or Union.  I would firmly support the
structuring of said primitives over a category based theory.

Concerning the compiler rewrite, I will most certainly seek your
advice when these issues become a practical concern.  I'm trying to
develop a `world view' of the features and facilities others would
like/expect.  Even if I cant implement all the features in one shot, I
can avoid coding the system into a corner so that future extensions
are feasible.


Thanks again!
Steve