Are `join` and` fmap join` consistent in Haskell (in terms of category theory)?

Question

My question arises from the first monad law in Haskell: join . fmap join = join . join join . fmap join = join . join join . fmap join = join . join

In Haskell / Category_theory, this law is shown in the following figure:

I am confused by the fact that this example uses type instances, not types. Because objects in the Hask category are types, not instances of them.

So, I tried to redraw this example using types, and here is what I got:

In this figure, both arrows ( join and fmap join ) lead to M(M(X)) . Is it the same object or two different M(M(X)) ?

Answer 1

I am confused by the fact that this example uses type instances, not types. Because objects in the Hask category are types, not instances of them.

The example uses an instance of the class, which itself is a type.

---

In Haskell, yes, this is the same object (type). Monad instances must be type constructors, and type constructors are injective. Then it should be pretty clear that

 X = X => M(X) = M(X) => M(M(X)) = M(M(X)) 

The trap here is that it means that they are the same type, not value. Just because fmap join and join can have their own types specialized for Monad m => m (m (ma)) -> m (ma) does not mean that they do the same.

They do not.

 ghci> (fmap join) [[[1],[2],[3]]] [[1,2,3]] ghci> join [[[1],[2],[3]]] [[1],[2],[3]] 

Not all category drawings should end with commuting diagrams. :)

Answer 2

It can be seen from the figure that fmap join and join create different values ​​of the same type. Thus, they do not match, although their composition with join ultimately produces the same values.

In category theory, epimorphism is a morphism of g such that f1 . g == f2 . g f1 . g == f2 . g f1 . g == f2 . g also implies f1 == f2 . In this case, we can see that join not an epimorphism, because although fmap join . join == join. join fmap join . join == join. join fmap join . join == join. join , it is not true that fmap join == join .