Deriving functor laws and properties from composition

[brucou]

Hi,

Here it is mentioned that functors, applicative functors, and monadic functors enables composition with a specific class of functions.

I could recover the equivalence between the monadic laws and the properties that must fulfill a composition operation (associativity, identity, closeness under operation, etc.) but I am stuck when I try to do the same for functors.

In the case of monads, we are dealing with functions $f: A -> M\ B$, for any morphism $M$ (that's the right name right?). So when looking for a composition operation, we are composing two functions of the same shape, we know the resulting shape.

However, the example with functors involves composing functions of different shapes. $f: A -> F\ B$, and $g: B -> C$. I am stuck as I can't even deduce what is the domain and codomain of $g \circ f$ from the properties of the composition operation.

Should I posit that $g \circ f$ is of the shape $A -> F\ Y$ and work from there? or can I deduce somehow for instance that the codomain of $g \circ f$ must be $F\ Y$ for some suitable $Y$?

[brucou]

Assuming that for a function F between types, and any function f between values, one can define an $fmap_F$ function, i.e.:

$$\forall F, \forall f: A \rightarrow F\ B, \forall g: B \rightarrow C, \exists fmap_F : (A \rightarrow B) \rightarrow (F\ A \rightarrow F\ B)$$

then $\circ$ defined as $g \circ f = (fmap\ g) \cdot f$ fulfills the composition laws iff $fmap$ fulfills the functor laws.

Let's show one direction: composition laws implies functor laws.

1. closure
   $fmap\ g : F\ B \rightarrow F\ C \implies \circ : (B \rightarrow C) \rightarrow (A \rightarrow F\ B) \rightarrow (A \rightarrow F\ C)$

In fact, this is not really a closure property? That looks more like an absorption property.

2. Identity
   $\exists Id_\circ, \forall f, Id_\circ \circ f = f \circ Id_\circ = f$

$\iff \forall f, (fmap\ Id_\circ) \cdot f = (fmap\ f) \cdot Id_\circ = f$

Applying this with $f=Id_\cdot$,
$$\implies (fmap\ Id_\circ) \cdot Id_\cdot = (fmap\ Id_\cdot) \cdot Id_\circ = Id_\cdot$$
$$\implies fmap\ Id_\circ = (fmap\ Id_\cdot) \cdot Id_\circ = Id_\cdot$$
$$\implies fmap\ Id_\circ = Id_\cdot$$

3. Associativity
   Same reasoning with writing the associativity laws with $f = Id_\cdot$, and observing that $g \circ Id_\cdot = fmap\ g$
   $$\implies fmap\ h \circ g = fmap\ h \cdot fmap\ g$$

[brucou]

What I can't show is that if we assume a composition operation $\cdot$ that fulfills the composition laws, then that composition function must be defined from some $fmap$.

[gcanti]

A category is defined by:

• objects ( $A$, $B$, $C$, ...)
• morphisms ( $f$, $g$, ...)
• a composition operation for morphisms ( $\circ$ )

The composition operation that can be used is always and only the one defined by the category being used, that is $\circ$.
There are no other forms of composition besides $\circ$.

Now, if I have a map between objects $F$ and two morphisms $f: A \rightarrow F B$, $g: B \rightarrow C$ there is no legal way
to compose them using $\circ$.

So we either give up or look for a concept of "composition" (I use quotation marks here to indicate that it is not the composition of the category but a custom composition concept that simply has a utilitarian purpose) that is "good" for our purposes.

To do this, we must somehow transform the involved morphisms because, as we have already said, there is no way to compose them using $\circ$.

However, there are many transformations that we can apply, for example to $g$, in order to make the morphism obtained after the transformation compose with $f$, which essentially means obtaining a new morphism whose domain is the codomain of the morphism $f$.

We could try to transform $g$ into a new morphism in these ways:

• $F B \rightarrow C$
• or $F B \rightarrow F C$
• or $F B \rightarrow C \times C$
• or ...

but which of these transformations is "good"? Each of them can be composed via $\circ$ with the morphism $f$, which should I choose?

The concept of functor is therefore a guide to make a choice, and it tells us that a good choice is $F B \rightarrow F C$

[brucou]

I understand that the functor, i.e. picking $FB \rightarrow FC$ from the list you mentioned is a valid choice as it creates interesting properties that are generic enough to be reused in a variety of contexts. The $FB \rightarrow C$ choice looks interesting too though. That looks like an extract of a comonad, or if I dared a copure of a coapplicative (assuming that exists in the first place, I only found mention of decisive functors in the litterature). Those Fs that you can enter and leave easily (e.g., with both pure and copure operations, that is both constructors and destructors) would be interesting creatures but I assume they are rare? For some reasons, they do not seem to be very discussed