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.
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.)