Live data from Hacker News

Category Theory Illustrated – Natural Transformations

abuseofnotation.github.io

21–30 of 86 posts

Re: Category Theory Illustrated – Natural Transformations

#21

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…

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

#22

Earlier 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.

You don't need category theory to connect dots with arrows, graph theory is enough for this.

Re: Category Theory Illustrated – Natural Transformations

#23

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…

> you can also specify that two mappings compose

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

#24

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

For me.. It's a very useful mental model for thinking about architecture & logic

Examples? I haven't really seen many applications of CT, even though I looked for them since I find the idea of CT interesting

Re: Category Theory Illustrated – Natural Transformations

#25
post #9

> 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

Re: Category Theory Illustrated – Natural Transformations

#27

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

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 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

#28
post #22

Earlier 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.

Category theory is actually a ‘simplified’ graph theory, i.e. you can see categories as a restricted class of graphs. E.G. ‘Category Theory for Computing Science’ introduces categories this way (a category is a directed graph with associative composition and identity; the free category on a graph is the graph with all identities and compositions filled in). But the restrictions (associative composition and identity) are harmless and natural for programming applications where there's always a notion of ‘do nothing’ or ‘do one thing after another’, and unlock a lot of higher structure.

Re: Category Theory Illustrated – Natural Transformations

#29

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

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…

I'd phrase this a tiny bit differently: monads give a model of effects in _impure_ languages and are important for that reason. The fact that Haskell chooses to emphasize monads in the language itself is cool, but their utility is not restricted to pure functional languages; quite the opposite! In a pure functional language you don't need to think about effects at all, and the only model you need is mathematical functions, which are much simpler.

Re: Category Theory Illustrated – Natural Transformations

#30
post #25
post #9

> 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

Insofar as ‘computation’ is about mapping one state or value to another state or value, it has a lot 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_.

Post reply on HN