Paul, On Mon, Aug 15, 2011 at 5:01 PM, you wrote: > On 15 Aug 2011, at 14:18, Bill Page wrote: > ... > I have been wondering if it's possible to think about Axiom's type system > using categorical language, and if the Axiom notion of a category can be > aligned in some way with mathematical categories.
Yes, and yes. > I find myself getting confused when looking at the various functions and type > constructors in the Axiom system, and I think to myself, can I hang all this > complexity on some kind of broad categorical framework. You mean replace something complex by something even more complex and abstract? ;) But of course complexity is a relative thing, right? At least in a categorical description of the Axiom type system you can count on rigor and generality. > > Such as, to a first approximation, functions between domains correspond to > arrows between objects in some category, type constructors that take domains > as arguments correspond to functors between categories, that sort of thing? Yes. In category theory terms FriCAS domains are objects in some overall category which is at least Cartesian closed (a mathematical category having objects and associated arrows that are the equivalent of tuples, unions and mappings as defined by SPAD). FriCAS functions are morphisms with source and target domains. Values are nullary functions from the terminal or empty domain into some target domain, e.g. zero() and one() in Integer. FriCAS categories are (in a loose sense) sub-categories of this overall category, i.e. subsets of domains which have a common set of "generators" in the sense of universal algebra (called exports in FriCAS). Yes type constructors are (in the same loose sense used above) functors between (sub)-categories. The subject of this thread is that domains can also be treated as values, i.e. as nullary functors into some (sub)-category. In other words there is a category in which all the FriCAS sub-categories are objects. It is possible to extend this analysis. > Are there any articles/papers on this subject? > I think the best description of all this was given by Saul Youssef. References here: http://axiom-wiki.newsynthesis.org/CategoryTheoryAndAxiom > Maybe I'm way off-base here, but I'd like to hear how other people manage > the complexity of the system in their heads. > Personally I think this does help to manage the complexity but of course it also raises some issues which strain the current capabilities of the FriCAS SPAD compiler (even Aldor) and the existing library, much of which was not specifically designed with mathematical categories in mind. Regards, Bill Page. -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To post to this group, send email to [email protected]. To unsubscribe from this group, send email to [email protected]. For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en.
