131–140 of 224 posts
I strongly recommend this presentation: "John Baez: "Symmetric Monoidal Categories A Rosetta Stone"[0]. It is easy to get lost in the ocean of theorems and definitions and overlook some powerful core concepts. [0] https://www.youtube.com/watch?v=DAGJw7YBy8E
Even though I've done much reading on the subject, and watched many of his lectures, my brain still jumps to music and Joan Baez.
Earlier quoted context omitted.
author here, for context, I do have a reasonable background in maths (algebra, analysis, statistics) at a CS master-ish level (self-taught and a long time ago, though), as well as spent quite some time with programming language / type theory when I was younger, and I do use monads quite a bit in my day to day programming. In fact, the fundamental algebra concepts (rings, groups, etc...) as well as fundamental CS theo…
How do you know analysis at a "CS master-ish level" (not sure what that means given it's a mathematical subject) but calculus did your head in? I'm not being judgmental but am just genuinely confused given that analysis is the foundation for calculus. :)
At least for American university-level calculus vs. American university-level analysis/topology over metric spaces.
> self-taught
Ah, makes more sense. I am also mostly self taught for most math. From my experience, I find it hard to believe after you did the exercises in PoMA, that calculus was harder.
Earlier quoted context omitted.
I see nothing in your link to justify what you say. Perhaps you can elaborate.
The way to run conjunctive SQL queries forward and backward is described in this paper, https://www.cambridge.org/core/journals/journal-of-functiona... , (also available on the arxiv), where they are referred to as query 'evaluation' and 'co-evaluation', respectively. We never would have been able to discover co-evaluation if not for category theory! The previous link includes this paper, and many others.
As someone with a maths degree, yet who admittedly hasn't looked into category theory beyond some basic notions, I still don't quite understand why anyone would want to learn category theory before e.g. abstract algebra or even just fundamental mathematical reasoning (definition, theorem, proof). Maybe I'm missing something but it seems to me that all you can study monads in programming languages without having to al…
Earlier quoted context omitted.
Sure, but what does the knowledge of something being an adjoint give you?
There are a lot of interesting properties: - Adjoints preserve limits/colimits. - Adjoint functors give rise to a monad - They are connected to universal morphisms
Earlier quoted context omitted.
Apologies for the jargon, but there isn't room in a comment box for a detailed explanation. "The Essence of the Iterator Pattern"[0] posed an open problem in type theory as to whether or not "lawful traversals", of type `∀ F:Applicative. (X -> F X) -> (B -> F B)` could appear for anything other than what is called a "finitary container"[1], B := ∃S. X^(P S) where the (P S) is a natural number (or equivalently a polyn…
This is a lot to digest, but I’m responding to this one because of I think this attempts to answer my question and because of your 4th reference. That being said I need to ask some questions. Would I be correct in saying — there are less complex objects, which are defined in category theory, that are useful in a generic way in combination with one another? If the answer to that question is yes, is there a place I loo…
The new "optics" people are have designed in reference 4 are not themselves "elements of category theory", but category theory provides the theoretical framework that these composable optics live in. Once that framework is identified, it becomes much easier to say "oh, this new optic definition I've just identified, fits into this framework, and so does this other optic, and so forth"
To make a loose analogy, one could imagine identifying triangles and cubes and such and such that have these rotational and reflective symmetries, and notice how you can compose those operations, and then see how performing specific shuffles of cards is also composable and has some properties similar to rotating cubes in that repeated operations have a certain period and other such things. Then when someone introduces you to group theory and says yes both the cube rotations and the card shuffling can all be seen as a group and group theory can be used to generically answer your questions about these otherwise seemingly very different operations. And then you start seeing that lots of things are groups, like that Rubik cube puzzle you have, or lines through an elliptic curve. Coming up with new optics is analogous to noticing various things are groups, a task that is much easier when you have group theory and know how to recognize a group when you see it.
That said, I think a better answer to your question may be in one of my later replies https://news.ycombinator.com/item?id=33806744: Category Theory has been useful for devising an entirely new (functional) programming abstraction, the theory of "optics" in my case. But for day-to-day programming you don't normally need to invent entirely new programming abstractions, you can just use the ones that have already been developed by the computer scientists.
Earlier quoted context omitted.
How do you know analysis at a "CS master-ish level" (not sure what that means given it's a mathematical subject) but calculus did your head in? I'm not being judgmental but am just genuinely confused given that analysis is the foundation for calculus. :)
Yeah, [edit: I doubt this]. I have a degree in math and cs. It sounds like parent comment doesn't really know analysis. The exercises in Rudin 1 are way harder than memorizing some rules to evaluate integrals. [Edit: at least for me; and I've never heard someone say the opposite before.] At least for American university-level calculus vs. American university-level analysis/topology over metric spaces. > self-taught A…
Looking at it now, I think maybe I just found it too boring to remember the tricks, and too tedious to not make mistakes, while I found coming up with proofs more "interesting" and requiring less rote memorization.
Earlier quoted context omitted.
In Ruby and many other languages, you have this idea of a string concatenation: "foo" + "bar" -> "foobar" "foo" + "" -> "foo" That makes it a monoid. Instead of talking about OOP patterns, knowing that the "+" operator is a monoid for string objects lets us write code that is composable. Similarly, with arrays: [:foo,:bar] + [:baz] -> [:foo,:bar,:baz] [:foo,:bar] + [] -> [:foo,:bar] Some language platforms will imple…
Most of us can go our whole careers without the "insight" that string concatenation is a "monoid". I don't know any languages that would balk at "foo" + "" or [a, b].concat([]). This all seems academic beyond belief.
Monoids are really simple, so you probably won't get a lot more examples there. But monads are a different story. Once you know the pattern, you really miss them. For example, Promises in Javascript are like painful versions of monads. There is a lot of special-case language support and reasoning around Promises that only apply to Promises. In a language with native support for monads, you could use the same code or libraries to handle patterns arising when using promises, as patterns arising with other monads like I/O.
In summary, if you never try it, you may never know or care what you're missing, but that doesn't mean you're not missing anything...
Earlier quoted context omitted.
> or even just fundamental mathematical reasoning (definition, theorem, proof). Logic and proof theory is actually one of the areas in math where category theory is most clearly useful. Intuitively, this is because reflexivity ("A leads to A") and transitivity ("A leads to B and B leads to C, hence A leads to C") are well-known rules of any kind of proof writing or indeed of argumentation in general, and they exactly…
I know a fair bit about logic and none of it involves any CT. That's not to say you can't find it in there somewhere as a unifying concept, but the fundamental theorems such as completeness and compactness of FOL, basic model theory, Gödel's theorems, etc. do not require any CT. Also, reflexivity, transitivity and symmetry just define an equivalence relation, no need for CT there.