On 25 October 2016 at 15:27, Bertfried Fauser <[email protected]> wrote: > > Hi Ralf, > > I agree with your reservations against the name functor (in the sense > of category theory) which is different from what map is doing. In your > signature it is clear that map is an > map part of a functor definition, hence given the following data: > > i) f: A -> B a map in a category C, with objects A,B > ii) a functor F : C --> D, which maps objects A,B,,... in category C to > objects F(A),F(B),... in category D > iii) we need to define maps in D from maps in C, hence > F( f:A --> B) |--> F(f) : F(A) --> F(B) [which is your signature] > iv) functoriality means that F( f o g) = F(f) o F(g) [where o is > the composition in C or D] > given this, one can compute maps F(f) in D by going back to C, > using the map f there. >
This of course just the standard definition of functor in category theory. The class Functor in Haskell is defined as follows class Functor F where fmap :: (A -> B) -> F A -> F B The 'fmap' operator obeys the following laws: fmap id = id fmap (p . q) = (fmap p) . (fmap q) where id is the identity function, p and q are arbitrary functions and . denotes composition. The Haskell Functor class implements a functor in the following category theory sense: In Haskell there is only one category where all objects and maps live. https://en.wikibooks.org/wiki/Haskell/Category_theory Given two objects 'A' and 'B' the Functor 'F' determines two new objects 'F A' and 'F B' Given a function 'f' in 'A -> B' fmap determines a function 'fmap f' in 'F A -> F B'. The Haskell Functor laws just describe standard categorical functoriality. > ... > So map is in my eyes an implementation detail which is not directly > mapped to the mathematical structure, as it is not (easily) composed > (as endofunctors can be). I do not see any problem with composing maps. > Further > more it implements only the part of the functor which deals with > morphisms, but all discussion here is set (element) bases and hence > categorically evil :< > There is nothing in the Haskell definition of Functor that is set or element based. The original proposed definition by oldk1331 <[email protected]> of Functor in FriCAS is )abbrev category FUNCTOR Functor Functor(S : Type) : Category == Type with map: (S -> S, %) -> % )abbrev domain A A A(S:Type): Functor(S) == add map(f:S->S,x:%):% == ... If we wanted we could use the equivalent definition map: (S -> S) -> (% -> %) This is equivalent to the Haskell case class Functor F where fmap :: (S -> S) -> F A -> F A for objects (domains) S and A. The more general case requires something a bit more complicated in FriCAS )abbrev package FUNCTOR2 FunctorPackage FunctorPackage(A : Type, B : Type, FA : Functor A, FB : Functor B) : Exports == Implementation where Exports == with map : (A -> B, FA) -> FB Implementation == add ... But the analogy with Haskell is clear. None of this is about actually implementing mathematical category theory in FriCAS which is a whole other subject, e.g. categories in Sage or the work of Saul Youssef in Aldor. This is just giving a mathematically sound definition of the notion of mapping a function over some "container-like" object which turns out to have a very close relationship to the notion of functor in mathematical category theory. Bill Page. -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/fricas-devel. For more options, visit https://groups.google.com/d/optout.
