Hacker News new | ask | show | jobs
by bubblyworld 599 days ago
I would like to second this take, as someone who found it very useful while writing up my masters (in logic). When you're working with objects that satisfy lots of universal laws (particularly algebras, logics, stuff like that) CT can be used to remove tons of "boilerplate" in your proofs for things that are basically trivial/routine but a pain to state and prove formally. As an example, imagine a construction where you extend the underlying language of some logic (like adding additional constant symbols in, for instance). Strictly speaking, to "transfer" results into this new logic you need to do a bunch of tedious proof to show that everything goes through the way you would expect. Category theory can make expressing and working with this class of thing (and many others) very expedient.

It's a bit like working in a framework that has great primitives for the stuff you do a lot. Like think dependency injection for constructing instances. Saves you tons of coding time in the long run.

Of course, this point of view is probably hard to appreciate from outside the priesthood =P.