[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] Unions in Spad
From: |
Stephen Wilson |
Subject: |
Re: [Axiom-developer] Unions in Spad |
Date: |
08 Jul 2007 23:57:16 -0400 |
User-agent: |
Gnus/5.09 (Gnus v5.9.0) Emacs/21.4 |
"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
- [Axiom-developer] Unions in Spad, Stephen Wilson, 2007/07/08
- Re: [Axiom-developer] Unions in Spad, Ralf Hemmecke, 2007/07/08
- Re: [Axiom-developer] Unions in Spad, Gabriel Dos Reis, 2007/07/11
- Re: [Axiom-developer] Unions in Spad, Bill Page, 2007/07/11
- Re: [Axiom-developer] Unions in Spad, Gabriel Dos Reis, 2007/07/11
- Re: [Axiom-developer] Unions in Spad, Bill Page, 2007/07/11
- Re: [Axiom-developer] Unions in Spad, Gabriel Dos Reis, 2007/07/11
- Re: [Axiom-developer] Unions in Spad, Bill Page, 2007/07/11
- Re: [Axiom-developer] Unions in Spad, William Sit, 2007/07/12
- Re: [Axiom-developer] Unions in Spad, Stephen Wilson, 2007/07/12
- Re: [Axiom-developer] Unions in Spad, Gabriel Dos Reis, 2007/07/12
- Re: [Axiom-developer] Unions in Spad, William Sit, 2007/07/12