30 ms·
Watched that guy's lectures and conference talks. While it's quite interesting and educative - I still don't get the "for programmers" part of it. I don't quite
by reykjavik 7y ago
Watched that guy's lectures and conference talks. While it's quite interesting and educative - I still don't get the "for programmers" part of it. I don't quite get how I would jump from understanding categories, morphisms, monoids etc. to building actually better systems. There are zero practical examples in his talks. Is it because i'm not using functional languages or what am I missing here?
- rubyn00bie 7y agoYeah, +100 I have this same problem in general. FWIW, the only real practical example I've seen (which has been rather serendipitous for me) is the "Seven Sketches in Compositionality" linked in the comments below applying category theory to databases. You can even play with the actual an implementation (written Java) to see some real world code here: https://github.com/CategoricalData/CQL https://github.com/CategoricalData/CQL Dunno if that helps your needs much but it was at least some kind of concrete starting point for me.
- philzook 7y agoBeing into functional programming helps quite a bit I think. In particular, category theory seems to nest well and illuminate some complicated uses of polymorphism and continuation passing style transformations. Categories are also a useful abstraction/pattern for designing interfaces to libraries. It's sort of a more mathematically flavored version of dataflow style libraries like simulink or gnuradio diagrams and stuff. Gluing together lego blocks and building up pipelines. I have been fiddling around with a categorical interface for solve linear equations which I think is pretty neat. http://www.philipzucker.com/linear-relation-algebra-of-circuits-with-hmatrix/ http://www.philipzucker.com/linear-relation-algebra-of-circu...
- d-d 7y agoThe practical takeaway for me is being able to see patterns and systems I never would have seen otherwise. I avoid a lot more pointless building; sometimes entire projects. The things I do end up creating come from a much deeper place of true need.
- reykjavik 7y agoThat is really interesting point. Could you give an example when you avoided project because of understanding of categories?
- d-d 7y agoI was able to see how the automation software I was designing would ultimately be an equivalent experience to its manual counterpart and thus be pointless to build. This reads like common sense but it wasn't; there were thousands of lower level factors. Studying the mechanism of analogy and "sameness" seems to help the mind with abstraction. Perhaps because it is the differences in data which reveal what is most useful to know when creating. In other words, I think a perspective that can see more of the similarities can "diff" and solve problems more quickly.
- co_dh 7y agoUnix pipeline a category, with text be object, and executable be morphisim converting text to text(monoid). Forth is a category, with stack as object, functions as morphisim. There are many examples. Best learn from haskell.
- Koshkin 7y agoI could never learn what pipeline is this way.
- crimsonalucard 7y agoI watched the first part of his lectures on category theory. Keep in mind I'm the furthest thing from a mathematician you can find. The feeling I'm getting when learning category theory is that if there was a formal theory for how to design programs. Category theory is it. Application is therefore not straightforward... You have to get really creative and think really hard to see the insights that category theory has to offer. The notion of a isomorphism and a functor and lifting was directly applicable to programming after I learned about it. Here's what happened: In postgresql there are specific library functions for dealing with specific types of json structures in the postgresql library. If your json blob doesn't fit the structured type parameter that the library function accepts you have to do some very awkward joins to convert the json into the right format which can cause massive slow downs. I use the notion of two isomorphic objects and the opposing functors between them to convert the json into a string functor. Then I did string manipulations to convert the serialized json into a different form of serialized json then re-lifted the serialized json back into the json functor. The converted json type fit the parameter of a library json function and thus the result was a query that executed 10x faster then the other implimentation. If I didn't know category theory the code would look absolutely crazy. I cast json to a string, replace a bunch of characters in the string then cast it back to json. The notion that a string can contain another type as a functor and the notion that string manipulations operations on serialized json have an isomorphic equivalent in "json space" was what allowed me to creatively come up with this optimization. Note that the json equivalent morphisms I needed do not actually exist in the postgresql implimentation but because of the isomorphism that exists between stringified json and actual json I can build the json morphisms I need by composing two opposing functors and a string manipulation operation. The thing about this though is that it's debatable whether or not you would actually need such "creativity" in a language that wasn't as terrible as SQL.
- philzook 7y agoCheck out Program Design by Calculation and The Algebra of Programming. Category theory and related formalisms do have a strong case to being a formal theory for designing/calculating programs http://www4.di.uminho.pt/~jno/ps/pdbc.pdf http://www4.di.uminho.pt/~jno/ps/pdbc.pdf https://themattchan.com/docs/algprog.pdf https://themattchan.com/docs/algprog.pdf
- shrimpx 7y agoOne guy Eugenio Moggi saw that the category theoretical "monad" could formalize "imperative programming" in pure functional languages by carrying a "world" parameter that represents the state being modified. Since then people have been trying hard to jam the rest of category theory into programming hoping to uncover similarly striking results, to no avail.
- curryhoward 7y ago> by carrying a "world" parameter that represents the state being modified From this, it's clear you've never read and understood Moggi's seminal paper. Monads are functors with some extra monoidal structure. The concept, and even Moggi's use of it in categorical semantics, has nothing to do with "worlds". The important realization is that there are many more monads than just the one hardcoded into one's programming language of choice. State, error handling, parsing, reading from an environment, backtracking, nondeterminism, mutable state, logging, probability, continuations, async/await, I/O, ...these are all just specific instantiations of the general interface of monads. Recognizing that allows you to build abstractions that work for any monad, rather than re-discovering and re-implementing the same idea for each one separately. It's been a remarkably fruitful area of research.
- LessDmesg 7y agoMonads are still programmable semi-colons, though. Yes, there are a lot of things you can program into a line-end symbol. Yes, some of those things are general and work for any already modded semi-colon. But it's still just programmable semi-colons: implicit, uncomposable, and frankly better left alone.
- jolux 7y ago>implicit You'll have to elucidate, I don't follow. >uncomposable Demonstrably false, see monad transformers. >better left alone. "Yeah, well, that's just, like, your opinion."
- 7y ago
- madhadron 7y agoSo here's a "folk theorem" that explains why you should care about such abstract structures. Take a 2x2 matrix with real elements (a b)(c d). If I take the space of all such matrices and put a uniform probability distribution over it, what is the probability of getting a matrix that is not invertible? Not invertible is det M = 0, or ac - bd = 0. I can solve for a in terms of b, c, and d, which shows that the non-invertible matrices are a 3 dimensional subspace of the 4 dimensional space, which has zero volume. So a matrix chosen at random is invertible. The folk theorem is in analogy with this: say I have a set of elements {a, b, c, ...}, and I describe mappings of various kinds that take some subset of tuples of the elements into other subsets. You can draw it as a directed multigraph. If you consider the space of all such graphs, how many of them generate "rich" or "regular" structure? For example, having a system where my mapping is defined over all elements is actually pretty restrictive. For a set of N elements, there are N-1 + N-2 + ... + 1 sets that are not defined over all elements. As N gets large, this dwarfs my one regular version. As I put in more operations and go to infinite sets of elements and add more regularity properties, this imbalance grows. So systems that have rich, regular structure are a zero volume subspace of the set of all such systems. Given this, suddenly the interest in the few dozen algebraic structures that algebraists of various kinds explore makes a lot more sense. They're following infinitely thin paths of structure through space. You start from a raw set with no operations. In one direction you trace through monoids, groupoids, semigroups, groups, rings, rigs, tropical rings, fields, vector spaces, modules, etc. In another you go through pre-orders, partial orders, chain complete partial orders, semilattices, lattices, etc. In another you go through categories, topological spaces, natural transformations, monads, arrows, topoi... Roughly, the groups, rings, fields path takes you through values that have regularity that looks vaguely like numbers. Orders and lattices take you through things that look like decomposition into pieces. Categories to topoi take you through things that look like sequences of operations and transformation. That the latter might be of interest to a programmer is fairly obvious from this point of view. So when someone says a monad is interesting, what they are trying to tell you is that it is the relevant data structure for describing an imperative program the way an array or list is the relevant data structure for describing an ordered sequence of numbers. The reason you care, then, is that once you have traced out these paths, when you are looking at a problem your brain will automatically try to draw you back towards the thread of regular structures. Sometimes you don't go to familiar ones. I ended up building an odd variation of lattices to describe genome annotations because of this, and it was an exercise in finding what about the domain drew me out of strict regularity rather than trying to find my way into it, which is a lot easier. Similarly, the entirety of the literature on eventual consistency in databases can be summarized as "make your merge operation the meet of a semi-lattice." If you've traced through that particular thread, then you can immediately think in a deep way about what kind of structure eventual consistency has and what the variations on it are.