5 ms·
One thing that has always bothered me is how people say that ideas from category theory can be useful while writing Haskell code. It's technically true, but rea
by orangea 4y ago
One thing that has always bothered me is how people say that ideas from category theory can be useful while writing Haskell code. It's technically true, but really only the most basic ideas — things which would be in the first chapter of a textbook on category theory, and which many might not even consider to be part of category theory itself. (For example, every type in Haskell is inhabited, which alone somewhat limits what you can say about it...)
And then there is also the fact that there is a huge difference between the skills and ideas that are useful for writing proofs in a theorem prover and those that are useful for writing quality software.
Also, anything having to do with homotopy type theory is even further removed from programming than regular type theory. Correct me if I'm wrong but I think that it is really only useful for helping prove theorems in homotopy theory, rather than being more generally useful for other kinds of math.
- remexre 4y agoUnivalence seems generally useful for verified software engineering, if we could get it in a system with regularity.
- klysm 4y agoI think a lot of concepts from category theory can be applied to every day programming in a lot of languages. Understanding how things compose helps you write better APIs.
- orangea 4y agoI don't mean any offense to you personally, but this kind of comment is why I hate internet discussions. You just said the opposite of what I said without adding anything new.
- Koshkin 4y agoBut it’s indeed true that > Understanding how things compose helps you write better APIs.
- orangea 4y agoWhich has nothing substantial to do with category theory.
- macrolocal 4y agoNah, here's a recentish overview: https://golem.ph.utexas.edu/category/2020/01/profunctor_optics_the_categori.html https://golem.ph.utexas.edu/category/2020/01/profunctor_opti...
- jnash 4y agoComposition is an old idea that predates Category Theory by a long shot.
- Koshkin 4y agoBut the real understanding of composability in all its complexity and generality has only come with (the more recent developments in) category theory.
- jnash 4y agoNope. It is just a different model for the same thing. You might find it enlightens your understanding of composition but it doesn't make it more "real" than any other model.
- alimw 4y ago> Correct me if I'm wrong but I think that it is really only useful for helping prove theorems in homotopy theory, rather than being more generally useful for other kinds of math. It seems a little immoral to select a foundation according to how "useful for helping prove theorems" it is...
- edflsafoiewq 4y agoWhat on earth else would you select it for?
- alimw 4y agoUnfortunately I can't find the link but somewhere out there I've seen one you'd like; a radically helpful theorem prover that advertises itself as the quickest and easiest way to prove anything. The joke is that everything is true. For those in this thread who are interested in HoTT and looking for a way in, I'll point out this series of online lectures (+ discord etc. in fact a school) beginning very soon and seemingly designed to provide that introduction. https://uwo.ca/math/faculty/kapulkin/seminars/hottest_summer_school_2022.html https://uwo.ca/math/faculty/kapulkin/seminars/hottest_summer...
- deleted 4y ago[deleted]