4 ms·
I am curious about category theory? Do you have any resources on where it can be applied?
by febin 6y ago
I am curious about category theory? Do you have any resources on where it can be applied?
- Twisol 6y agoI'm no expert, so the best I can do is point you to the research community gathering around applied category theory. * A conference series + workshop: https://www.appliedcategorytheory.org/ https://www.appliedcategorytheory.org/ * A journal: https://compositionality-journal.org/ https://compositionality-journal.org/ Check out some of the people involved in organizing these events. Names I've followed include John Baez, Pawel Sobocinski, and Tai-Danae Bradley (all of whom are amazing educators; check out their work!). Tai-Danae Bradley wrote a pamphlet on applied category theory which is very approachable: https://arxiv.org/pdf/1809.05923.pdf https://arxiv.org/pdf/1809.05923.pdf . Also check out Jules Hedges' thoughts on the importance of compositionality: https://julesh.com/2017/04/22/on-compositionality/ https://julesh.com/2017/04/22/on-compositionality/ .
- harry8 6y agoHaskell. To do io you need monads. There's come from category theory. Haskell is great fun to learn, very different, focus on abstractions and abstractions of abstractions. One the one hand i highly recommend it. On the other the vast majority of people learning it never do any useful work at all in haskell. (This last statement will probably excite the haskell zealots whom I would encourage to reply with evidence.) There are about 5 programs i know if that you might use written in haskell for a purpose other than programming a computer. Anyway category theory definitely comes up in lazy, pure functional programming. A lot.
- Twisol 6y agoAs a great fan of Haskell myself, I would clarify that Haskell needs monads because of the (pure functional) restrictions it sets for itself, not because I/O itself fundamentally requires explicit monads. (Haskell itself supposedly used a lazy-list approach to input and output before monads caught on -- something like `main :: [Response] -> [Command]`, I think.) That being said, when you explicitly model side effects, you invariably end up with some kind of monad in your model. Food for thought: in a logic programming setting, where your domain is some flavor of partially ordered set, monads are closure operators (a kind of monotone function). Closure operators give a cool foundation for the semantics of certain kinds of logic paradigms, such as concurrent constraint programming.
- mikorym 6y agoThis statement that you made—about side effects requiring monads—do you know a proof for that? I come from the other side, Milewski's book is to me "Functional Programming for Category Theorists".
- Twisol 6y agoNope, no proofs :) Formalizing questions like this is one reason why I'm interested in category theory, so I don't think I have the tools to dig into this right now. But... "side effect" literally maens it doesn't show up in a normal input/output function signature, and in a pure functional language like Haskell, there are no side effects. Monads are a particular way of explicitly capturing side effects as a "separate" kind of thing from the function output using a particular species of functor. I suppose my statement was a bit strong in that regard. Monads tend to arise very often in the way we build systems, but that doesn't mean they're the only way to cope with side-effects. It does seem likely that any way to capture "alternate outputs" from a function will end up looking like A -> T(B) in some category, though. (Incidentally, if "A -> T(B)" looks funky, think about polynomials `f(x)` -- the function symbol `f` is just a placeholder for some expression involving the free variable `x`. Could be `A -> (B, String)`. The monad laws only make sure you have some foundation for reasoning about the extra type structure being added in by `T`.)
- mikorym 6y agoDoes this mean that you use a monad instead of a function?
- Twisol 6y agoFirst, a clarification: when looking at a monadic action `f : A -> T(B)`, the monad here is just `T`. The action itself is still just a function. The monad `T` lets you add some extra structure onto your usual output type in a principled way. That being said, it's true that I'm using `T` itself in a function-like way. Category theory does blur the lines between the two ideas: monads are "functors" with some extra structure, and functors are ("just") functions between categories that preserve categorical structure. But it's critical to notice here (and it's apparent from the type `f : A -> T(B)`) that `T` is not the same kind of function that `f` is. `f` lets you move from one type to another, by mapping each value in one to a value of another. `T` lets you move from a whole category to another category, by mapping each object/type in one to an object/type of another, and mapping each arrow/function in one to an arrow/function of another. In other words, monads occur at the type level, whereas functions occur at the value level [1]. That means that, colloquially, you can't just use a monad "instead of" a function, any more than you can use "Integer" instead of "42". But as I alluded to above, monads over partial orders are closure operators, and we can often model the evolution of data over time as a partial order. So in that domain, monads literally are functions, and the "side effect" of a closure operator is mutably updating a cell by moving its contents up in the order. If you model the evolution of data as a partial order, you can indeed obtain monads that more closely resemble normal functions. But a partial order is just a particular kind of category, so even here we've built a separate little domain over which our monad exists. (Of course, functors are all about crossing those domains in principled ways.) [1] That's why it's not "IO ()" or "Maybe Int" that are monads; it's "IO" and "Maybe" themselves, which are well-behaved functions from types to types.
- gsjbjt 6y agoDavid Spivak and Brendan Fong have been doing lots of work at MIT to evangelize applied category theory. See their recent books/classes: Seven Sketches in Compositionality: An Invitation to Applied Category Theory https://arxiv.org/abs/1803.05316 https://arxiv.org/abs/1803.05316 Applied Category Theory mini-course: https://ocw.mit.edu/courses/mathematics/18-s097-applied-category-theory-january-iap-2019/ https://ocw.mit.edu/courses/mathematics/18-s097-applied-cate... Programming with Categories mini-course (with Bartosz Milewski): http://brendanfong.com/programmingcats.html http://brendanfong.com/programmingcats.html
- viridi 6y agoPerhaps Category Theory for Programmers? https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ https://bartoszmilewski.com/2014/10/28/category-theory-for-p... There is also a playlist on Youtube https://www.youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ https://www.youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbm...