On Thursday, May 11, 2006 7:14 PM Gabriel Dos Reis wrote: > > Ralf Hemmecke writes: > > [...] > > | But of course, I could live with that identification if it > | is clearly documented that ()->Cat can be identified with Cat. > | Where are our category experts? I believe there is a distinction > | here, n'est pas? > > From Category Theory point of view, a constant x of type T > is the same as the (unique) morphism x : 1 -> T, where 1 is > the one-point set.
The relevant object here is the initial object 0 in a complete Cartesian closed category (CCCC), not the terminal object 1. http://en.wikipedia.org/wiki/Initial_object It is quite reasonable I think to let () denote the initial object in the CCCC associated with the categorical semantics of Aldor. The definition of initial is that: there exists precisely one morphism () → X for each object X. So in a sense any "categorical" distinction between the morphism and co-domain object is not likely to be of much interest. > > Now, I also understand that beyond the name, Aldor's categories > are not mathematical categories; so... I think that is an over statement. There is a considerable similarity between categories in Aldor and mathematical categories. But that is irrelevant. Any "sufficiently complex" programming language must have the structure of a complete Cartesian closed category. > > My practice of functional programming suggests that the > identification is useful in many cases, than keeping the > artifice. But YMMV. > I think this identification can be justified from a mathematical point of view. Regards, Bill Page. _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
