I don't understand how learning the definition of a limit, colimit, adjunction, pushforwards, pullbacks, equalisers, co-equalisers and the Yoneda lemma, can help you write code. But I'm willing to be enlightened.
Some starting points: tuples are categorical products (an example of limits), sum types are categorical coproducts (an example of colimits), effects are often monadic and monads arise from adjunctions, the Yoneda lemma tells you that if you have "f a" and "a -> b" and you know nothing more about the "a" then all you can do is fmap the function over the functorial value.
Sure, knowing this doesn't "help you write code" in the same way that knowing "you press the keys on the keyboard to get text to appear on the screen" but I've found this way of thinking to be beneficial to some degree when programming.
But I think that eru is trying to emphasise that one should learn how to program first and then use category theory as a tool to organise your understanding.
Do you think category theory is more useful than type theory or logic?
I’ve personally gotten a lot more out of treating tuples as product types or logical AND, and disjoint unions as sum types or logical OR, as opposed to categorical limits.
(Basically, what’s the extra value added from Curry-Howard-Lambek, as opposed to just Curry-Howard, in terms of programming?)
(I’m not trying to be argumentative, I’m genuinely curious.)
I would put category theory very far down the list of things a programmer should learn. Once a programmer has learned a lot of other things about programming, category theory can act as a good organisational and explanatory tool.
As I also tried to say earlier, in practice I suggest learning programming first, and then using the likes of category theory to organise your understanding.
