[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] Unions in Spad
From: |
Bill Page |
Subject: |
Re: [Axiom-developer] Unions in Spad |
Date: |
Sun, 8 Jul 2007 23:37:06 -0400 |
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.
- [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