Gaby, I think my disagreement with you about whether List is an "endofunctor" is not very fundamental. Instead it is mostly a matter of terminology. My starting point is the mathematical definition of endofunctor in category theory. But as someone else posted to this list recently: category theory is in large part just a change in terminology - new language for things that we already think we understand. But I would dispute the claim that it is therefore of only limited or no interest. It seems to me that category theory provides a way of "slicing" or fixing terminology so that many things that did not seem that similar (or complimentary) are suddenly seen as essentially the same (or precisely the opposite).
In this case being strict about the definition of endofunctor necessitates the introduction of another functor which is normally implicit in Axiom. From your comments below it seems that you would prefer to absorb this implicit functor into what is referred to as type satisfaction in Axiom and consider this to be part of the definition of endofunctor itself. Conceptually there is nothing wrong with this except it does considerably weaken the concept of endofunctor and thereby misses the opportunity to identify a situation which arises very often in category theory: adjunction. Ref: http://en.wikipedia.org/wiki/Adjoint_functors I guess whether this is important or not depends on how strongly one believes that category theory has something important to say about computer algebra and about Axiom in particular. At this point I am still a believer. On Tue, Nov 15, 2011 at 2:16 PM, Gabriel Dos Reis wrote: > Bill Page writes: > > | One clarification. Actually despite what Gaby wrote in an earlier > | email, I still don't think it is quite correct to claim that a functor > | such as List is an endofunctor, at least not in the category-theoretic > | sense. > > Unless, you have a very exotic definition of endofunctor, A common definition of endofunctor is that it is a functor that maps a category to itself. > List(S) satisfies Type for all S that satisfies Type. How less "endofunctor" > can that be? > Type satisfaction has nothing to do with being an endofunctor. > | The reason is that it is defined as follows: > | > | List(R:Type): Join(ListAggregate(R), ... ) > | > | The source category of List, i.e. Type, is not the same as the target > | category of List, i.e. Join(ListAggregate(R), ... ). > > The target is included in Type, and that is all that is needed to > satisfy the notion `endofunctor'. Here is a counter example: FreeGroup is a functor with source SetCategory and target Join(Group, ... ). Group satisfies SetCategory (a group is a set with extra structure) so "the target is included in the source". In Axiom we can define a domain constructor such as FreeGroup FreeGroup Symbol But FreeGroup is not an endofunctor. To treat it as such we need a forgetful functor that forgets that extra structure added to Group. Of course such functors are always implicit in Axiom but they are very important in terms of category theory. The FreeGroup functor and this implicit forgetful functor are adjoint functors. There composition is an endofunctor. Ref: http://en.wikipedia.org/wiki/Monad_%28category_theory%29 >From this point of view the List functor is essentially equivalent to the FreeMonoid functor (as a monad). One might object that a List is a "data structure" while a FreeMonoid is a higher-level mathematical abstraction. This distinction is made fairly often in Axiom. FreeMonoid does in fact use a form of List structure as it's internal representation. But it seems to me that from a purely formal point of view there is no difference. http://en.wikipedia.org/wiki/Monads_in_functional_programming#Collections > Being an endofunctor does not require surjectivity! > That is correct but it is irrelevant. Regards, Bill Page. ------------------------------------------------------------------------------ All the data continuously generated in your IT infrastructure contains a definitive record of customers, application performance, security threats, fraudulent activity, and more. Splunk takes this data and makes sense of it. IT sense. And common sense. http://p.sf.net/sfu/splunk-novd2d _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
