[HN Gopher] Category Theory: Lecture Notes and Online Books
___________________________________________________________________
Category Theory: Lecture Notes and Online Books
Author : coalgebraic
Score : 118 points
Date : 2021-12-30 07:17 UTC (15 hours ago)
(HTM) web link (www.logicmatters.net)
(TXT) w3m dump (www.logicmatters.net)
| meiji163 wrote:
| The best book I've found for a non-math audience is Fong &
| Spivak, 7 Sketches in Compositionality.
| JosephHatfield wrote:
| Thanks for the recommendation. Found it available for free
| download at David Spivak's homepage on MIT's Math department
| website
| euroderf wrote:
| N00b question here. Does the mathematical characterization of
| category theory relate in any way to the bridges that the
| Langlands program is building ?
| Koshkin wrote:
| Well, one of the well-known category theorists has said [0],
|
| > _I've never succeeded in understanding the slightest thing
| about it._
|
| [0]
| https://golem.ph.utexas.edu/category/2010/08/what_is_the_lan...
| rg111 wrote:
| 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.
|
| 3. ToC book by Sipser.
|
| You get the idea.
| ryan93 wrote:
| Category theory seems like a "meme" interest among programmers.
| DaiPlusPlus wrote:
| 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.
| elnatro wrote:
| I find this topic fascinating but hard to start with.
|
| Does anyone have any non-Haskell example of category theory?
| Something that shows why is useful with a use-case.
| vkk8 wrote:
| 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.
|
| 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.
| meiji163 wrote:
| > I'm not sure how useful category theory actually is in the
| example cases.
|
| It's hard to say that category theory is "applied" to this or
| that problem. you'll hear many mathematicians call it
| "abstract nonsense" half-jokingly. More than anything it's a
| unified way of talking about mathematical structures that
| gives you a certain point of view (which is where it might be
| useful).
| alde wrote:
| 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.
| Koshkin wrote:
| This may be true if you take one concept (category) in
| isolation. But the power of category theory is in revealing
| hidden analogies between different concepts. Which is why it
| is an important tool in the areas like algebraic topology.
| Epa095 wrote:
| Freeman Dyson said:
|
| >Some mathematicians are birds, others are frogs. Birds fly
| high in the air and survey broad vistas of mathematics out to
| the far horizon. They delight in concepts that unify our
| thinking and bring together diverse problems from different
| parts of the landscape. Frogs live in the mud below and see
| only the flowers that grow nearby. They delight in the
| details of particular objects, and they solve problems one at
| a time. Mathematics needs both birds and frogs. Mathematics
| is rich and beautiful because birds give it broad visions and
| frogs give it intricate details.
|
| It is my impression that those loving category theory are
| predominantly birds. I am a frog, and never really got the
| love for category theory.
| mdm12 wrote:
| 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.
|
| [1] https://fsharpforfunandprofit.com/posts/recipe-part2/
| cashsterling wrote:
| 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.
| lapinot wrote:
| 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.
|
| 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.
| DarylZero wrote:
| Haskell is why it's relevant =D
| lapinot wrote:
| For haskell programmers most likely! Just like there's only
| the obvious way in which groups are useful for speed
| cubers.
| Twisol wrote:
| 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.)
|
| [0] https://fsharpforfunandprofit.com/rop/
|
| [1] https://blog.ploeh.dk/2017/11/13/endomorphism-monoid/
| Twisol wrote:
| That said, Spivak's work on framing databases in terms of
| categories [2] is pretty fascinating, and might be worth
| poking at.
|
| [2] http://blog.ezyang.com/2010/06/databases-are-categories/
| Jhsto wrote:
| This series has some C++ examples alongside Haskell:
| https://bartoszmilewski.com/2014/10/28/category-theory-for-p...
| and acquirable as a PDF at https://github.com/hmemcpy/milewski-
| ctfp-pdf
___________________________________________________________________
(page generated 2021-12-30 23:02 UTC)