What's the thing with category theory? I see this topic discussed quite frequently here but I don't get it why people are so into it
Category theory is what you get when you take mappings instead of sets as the primitive objects of your universe. At first this might seem a perverse thing to do as mappings seem more complex than sets, but that is just because traditionally mappings have usually been defined in terms of sets. In set theory you can specify that two sets be equal and you can also specify that one set be an element of another. In categ…
Category Theory Illustrated – Natural Transformations
21–30 of 86 posts
Re: Category Theory Illustrated – Natural Transformations
#22Earlier quoted context omitted.
Category theory is what you get when you take mappings instead of sets as the primitive objects of your universe. At first this might seem a perverse thing to do as mappings seem more complex than sets, but that is just because traditionally mappings have usually been defined in terms of sets. In set theory you can specify that two sets be equal and you can also specify that one set be an element of another. In categ…
So category theory is really the theory of composition of mappings. I conjecture that all programming can be seen as just the composition of mappings. If this is correct then category theory is a theory of programming.
Re: Category Theory Illustrated – Natural Transformations
#23What's the thing with category theory? I see this topic discussed quite frequently here but I don't get it why people are so into it
Category theory is what you get when you take mappings instead of sets as the primitive objects of your universe. At first this might seem a perverse thing to do as mappings seem more complex than sets, but that is just because traditionally mappings have usually been defined in terms of sets. In set theory you can specify that two sets be equal and you can also specify that one set be an element of another. In categ…
Two mappings with corresponding domain/codomain have to compose by definition of a category. It's not something you can specify.
Re: Category Theory Illustrated – Natural Transformations
#24What's the thing with category theory? I see this topic discussed quite frequently here but I don't get it why people are so into it
For me.. It's a very useful mental model for thinking about architecture & logic
Re: Category Theory Illustrated – Natural Transformations
#25> In the course of this book, we learned that programming/computer science is the study of the category of types in programming languages. This is a golden quote.
Re: Category Theory Illustrated – Natural Transformations
#26Re: Category Theory Illustrated – Natural Transformations
#27What's the thing with category theory? I see this topic discussed quite frequently here but I don't get it why people are so into it
The Curry-Howard "isomorphism" (slogan: propositions are types, proofs are programs/functions) map code to logic in a categorical way described first by certain book of Lambek-Scott with uses in formal software verification.
Categories provide abstraction. You first distill the behavior of how Haskell (or you other pet functional language) work with Hask, the category of Haskell types, and then you can apply your abstract distillate to other categories and obtain task-oriented, tailored computing concepts that enrich bare language capabilities, providing applications including 1) probabilistic programs 2) automatic differentiation. Conal Elliott has very concrete work along this lines. When he speaks of CCCs (following Lambek) he alludes to cartesian closed categories, the crucial property of having a type constructor for function spaces and higher order functions. See his "compiling to categories" for a very concrete, hands-on feel. Another application he shows is in hardware synthesis (baking your functional algorithm to a netlist of logical gates for automating the design of custom hw accelerators).
In short, why categories? computational effects, formal verification and the equivalence of simply-typed lambda-calculus with cartesian closed categories, with lambda-calculus being the backbone of functional programming language semantics.
Re: Category Theory Illustrated – Natural Transformations
#28Earlier quoted context omitted.
So category theory is really the theory of composition of mappings. I conjecture that all programming can be seen as just the composition of mappings. If this is correct then category theory is a theory of programming.
You don't need category theory to connect dots with arrows, graph theory is enough for this.
Re: Category Theory Illustrated – Natural Transformations
#29What's the thing with category theory? I see this topic discussed quite frequently here but I don't get it why people are so into it
Its of course the theory behind monads that since Eugenio Moggi are used to model computational effects in pure functional languages. Effects such as state, optional return types (used in turn for error handling) (maybe monad), input/output (reader writer monad) and others. Beyond effects, Wadler used monads for parsers (monadic parsing). The Curry-Howard "isomorphism" (slogan: propositions are types, proofs are prog…
Re: Category Theory Illustrated – Natural Transformations
#30> In the course of this book, we learned that programming/computer science is the study of the category of types in programming languages. This is a golden quote.
It's also wrong, since computer science is traditionally mostly about computation, which has nothing to do with CT
The question of whether CT is _useful_ for studying computation is different, and there are certainly other lenses you can see computation through that some people would argue are better. But it's hard to deny that they're _related_.