Seven Sketches in Compositionality is easily the best book to get started on Category Theory.
Learning something becomes highly fun and enjoyable when the authors/lecturers are deliberately trying to make it so.
Most books on anything serves to document something and looks like accumulated notes that are an overt attempt to impress the authors' peers. There is no focus on actually teaching.
This book is not like that. This book focuses entirely on teaching, tries deliberately so that you can learn.
Some other books that I have come across in my life are:
1. Intro to Electrodynamics by Griffiths
2. High School Physics book by Halliday, Resnick, Walker.
This might be an unpopular opinion, but category theory isn't very useful at low levels of abstraction. It is an elegant mental framework/model that can be used to generalize many concepts, but in my experience such generalizations rarely give additional insights about the concept it is generalizing.
Seven Sketches in Compositionality by Spivak and Fong (https://math.mit.edu/~dspivak/teaching/sp18/7Sketches.pdf) is supposed to be very practical. It includes many examples, but I'm not sure how useful category theory actually is in the example cases.
There is the theory of monotone co-design (https://co-design.science/index.html) which is formulated using category theory. It seems pretty practical.
I'm not very knowledgeful of any of these subjects, but I, like you, got somewhat interested in category theory and tried to find how and where it's used some time ago. These are the main things I found.
This feels to me like "is there any non rubik's cube example of group?". Category theory is a mathematical tool used by mathematicians and built for mathematicians, so you'll have trouble understanding why it's concretely relevant anyway if you're not in the business of doing maths :D The main motivation is that it's a good language for describing some kinds of objects and writing proofs about them.
I'm personaly using category in the field of logic and language semantics (describing and proving stuff about notions of equivalence between programs, results like language X can interpret language Y with such and such fidelity). At a high level, i think category theory is useful in that realm because it enables to make up new structures (algebraic structures, think some set with operations and laws) which will be specific to you (won't be something well known like ring or whatever) but thanks to category theory you'll already have results on these structures because you'll show that they have some generic constructions.
In general category theory sometimes enables mathematical statements to drastically cut down on unimportant assumptions, getting at the real core of some theorem. By doing that, you're enabling other to reuse some result in settings which are "kinda similar", where "morally stuff work in the same way", but where the classical definition would have been too rigid.
I feel like Scott Wlaschin uses an effective model of teaching concepts closely related to category theory without intimidating learners with mathematical definitions and verbiage. Railway oriented programming is a good example.[1]
My personal opinion is that category theory's main contribution to computer science is aiding composability in strongly typed languages in a type-safe, elegant manner. In the end, software is about breaking down a problem into smaller pieces, implementing and testing them, and them putting the pieces back together. Concepts from category theory provide a rigorous foundation for such compositions.
Cambridge Quantum Computing applies Category Theory to development of quantum computing algorithms. Recent paper by Bob Coecke: https://arxiv.org/abs/2110.05327. Look up more papers by Bob Coecke and co-authors on Arxiv.
Cambridge Quantum Computing and Honeywell Quantum Solutions recently merged to form Quantinuum. I work on the hardware side at Quantinuum. I don't actually use or apply Category Theory on a day to day basis but I know it is useful.
I find it most useful as a kind of conceptual organization. It's not something you'd directly solve problems with, but rather a way of organizing your work on the solutions. In that sense, it's much like software architecture -- you don't directly solve problems with architecture, either, but you do want an architecture that supports you when you need to make changes or grapple with a large or complex problem domain.
Unfortunately, that's also why most resources directly on category theory are deeply wedded to pure mathematics -- it's an architectural form that has been developed by mathematicians to organize their own constructions. Folks like Scott Wlaschin [0] and Mark Seemann [1] have, I think, much more success in teaching categorical concepts in a software context, but since their material is often so far removed from category theory "proper" (intentionally and for good reason), they don't really paint much of a path toward category theory themselves.
(I've recently been learning Agda, a dependently-typed language / proof assistant, and it's kind of shocking how often refactoring my proofs lead to more "obviously categorical" concepts. I really think there's something to this category-theory-as-mathematics-architecture angle.)
I wrote this article[0] as part of my own journey to understand monads and category theory.
I think you may find it helpful. It has a practical use case that builds up an intuitive
model to a new monad. It goes through a few solutions for a stated problem which solve increasing requirements and eventually coalesces into writing a new monad as a complete solution to resolve all the built up requirements.
Within the applied category realm where seven sketches lives, there are low-level concrete industrial applications that are becoming increasingly dominant with key industry players in quantum tech. The most known one is ZX-calculus which is explicitly used in things like compiler optimisation, error-correction, translations between computational models etc. This might be the 1st time that CT is playing a central role in a new technology. The reason is the high-level connotation that has been pushed far too long concerning category theory, originating in its abstract mathematical origins.
N00b question here. Does the mathematical characterization of category theory relate in any way to the bridges that the Langlands program is building ?
I have read and understood enough Category Theory to realise that it is kinda fun/interesting if you enjoy abstract math. But it won’t make you a better software (or Haskell) developer. I would instead recommend learning Coq/Lean/Idris/Agda to move up the abstraction level from Haskell, while still learning things that are relevant to developing software.
I have some interest in the topic (thanks to Arraycast and Conor Hoekstra) and bought to Mock a Mockingbird by Raymond Smullyan, however it is still a bit too involved for my small brain.
On the other hand, I am very much enjoying How to Bake Pi by Eugenia Cheng, which is a few levels down in difficulty.
It is, because modern programming languages today are far more expressive than previous generations of languages are, with powerful type-systems - and languages' type-systems are grounded in category-theory (and group-theory, and type-theory, and set-theory).
Modern languages are our tools, and you can't use your tools effectively without understanding them, and you can understand them better by understanding their mathematical underpinnings.
-------------
Disregarding the comparatively more esoteric languages like Haskell, consider TypeScript, Rust, Haxe, and to an extent: Kotlin and Scala: you can take a self-taught (i.e. non-CS/SE graduate) programmer and eventually they'll figure their way through, and eventually grok, that languages' type-system - and hey-presto, you've just unwittingly taught someone something an entire course of graduate-level abstract mathematics would do, and been productive in the process.
[+] [-] rg111|4 years ago|reply
Learning something becomes highly fun and enjoyable when the authors/lecturers are deliberately trying to make it so.
Most books on anything serves to document something and looks like accumulated notes that are an overt attempt to impress the authors' peers. There is no focus on actually teaching.
This book is not like that. This book focuses entirely on teaching, tries deliberately so that you can learn.
Some other books that I have come across in my life are:
1. Intro to Electrodynamics by Griffiths
2. High School Physics book by Halliday, Resnick, Walker.
3. ToC book by Sipser.
You get the idea.
[+] [-] elnatro|4 years ago|reply
Does anyone have any non-Haskell example of category theory? Something that shows why is useful with a use-case.
[+] [-] alde|4 years ago|reply
[+] [-] vkk8|4 years ago|reply
There is the theory of monotone co-design (https://co-design.science/index.html) which is formulated using category theory. It seems pretty practical.
Then there's topological data analysis, which is clearly a practical subject, and can be formulated in terms of category theory: https://en.wikipedia.org/wiki/Topological_data_analysis
I'm not very knowledgeful of any of these subjects, but I, like you, got somewhat interested in category theory and tried to find how and where it's used some time ago. These are the main things I found.
[+] [-] lapinot|4 years ago|reply
I'm personaly using category in the field of logic and language semantics (describing and proving stuff about notions of equivalence between programs, results like language X can interpret language Y with such and such fidelity). At a high level, i think category theory is useful in that realm because it enables to make up new structures (algebraic structures, think some set with operations and laws) which will be specific to you (won't be something well known like ring or whatever) but thanks to category theory you'll already have results on these structures because you'll show that they have some generic constructions.
In general category theory sometimes enables mathematical statements to drastically cut down on unimportant assumptions, getting at the real core of some theorem. By doing that, you're enabling other to reuse some result in settings which are "kinda similar", where "morally stuff work in the same way", but where the classical definition would have been too rigid.
edit: concretely about these generalizations: if you know about monoids, then look at https://en.wikipedia.org/wiki/Monoid_(category_theory) which is a categorification of it.
[+] [-] mdm12|4 years ago|reply
My personal opinion is that category theory's main contribution to computer science is aiding composability in strongly typed languages in a type-safe, elegant manner. In the end, software is about breaking down a problem into smaller pieces, implementing and testing them, and them putting the pieces back together. Concepts from category theory provide a rigorous foundation for such compositions.
[1] https://fsharpforfunandprofit.com/posts/recipe-part2/
[+] [-] cashsterling|4 years ago|reply
Cambridge Quantum Computing and Honeywell Quantum Solutions recently merged to form Quantinuum. I work on the hardware side at Quantinuum. I don't actually use or apply Category Theory on a day to day basis but I know it is useful.
[+] [-] Twisol|4 years ago|reply
Unfortunately, that's also why most resources directly on category theory are deeply wedded to pure mathematics -- it's an architectural form that has been developed by mathematicians to organize their own constructions. Folks like Scott Wlaschin [0] and Mark Seemann [1] have, I think, much more success in teaching categorical concepts in a software context, but since their material is often so far removed from category theory "proper" (intentionally and for good reason), they don't really paint much of a path toward category theory themselves.
(I've recently been learning Agda, a dependently-typed language / proof assistant, and it's kind of shocking how often refactoring my proofs lead to more "obviously categorical" concepts. I really think there's something to this category-theory-as-mathematics-architecture angle.)
[0] https://fsharpforfunandprofit.com/rop/
[1] https://blog.ploeh.dk/2017/11/13/endomorphism-monoid/
[+] [-] bern4444|4 years ago|reply
I think you may find it helpful. It has a practical use case that builds up an intuitive model to a new monad. It goes through a few solutions for a stated problem which solve increasing requirements and eventually coalesces into writing a new monad as a complete solution to resolve all the built up requirements.
[0] https://sambernheim.com/blog/building-a-monad
[+] [-] Jhsto|4 years ago|reply
[+] [-] bob_coecke|4 years ago|reply
Bob Coecke, Chief Scientist, Quantinuum.
[+] [-] euroderf|4 years ago|reply
[+] [-] Koshkin|4 years ago|reply
> I’ve never succeeded in understanding the slightest thing about it.
[0] https://golem.ph.utexas.edu/category/2010/08/what_is_the_lan...
[+] [-] mbrodersen|4 years ago|reply
[+] [-] OracB7|4 years ago|reply
On the other hand, I am very much enjoying How to Bake Pi by Eugenia Cheng, which is a few levels down in difficulty.
[+] [-] meiji163|4 years ago|reply
[+] [-] JosephHatfield|4 years ago|reply
[+] [-] ryan93|4 years ago|reply
[+] [-] DaiPlusPlus|4 years ago|reply
Modern languages are our tools, and you can't use your tools effectively without understanding them, and you can understand them better by understanding their mathematical underpinnings.
-------------
Disregarding the comparatively more esoteric languages like Haskell, consider TypeScript, Rust, Haxe, and to an extent: Kotlin and Scala: you can take a self-taught (i.e. non-CS/SE graduate) programmer and eventually they'll figure their way through, and eventually grok, that languages' type-system - and hey-presto, you've just unwittingly taught someone something an entire course of graduate-level abstract mathematics would do, and been productive in the process.