"Bill Page" <[EMAIL PROTECTED]> writes: > On 08 Jul 2007 22:27:00 -0400, Stephen Wilson wrote: > > ... > > "Bill Page" <[EMAIL PROTECTED]> 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 mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer