Category Theory Illustrated – Natural Transformations(abuseofnotation.github.io) |
Category Theory Illustrated – Natural Transformations(abuseofnotation.github.io) |
Heraclitus was before Parmenides and said that everything changes. Parmenides said that nothing changes, and then the atomists, most prominently Democritus, synthesised these two points of view by saying that there are atoms which don't change, but all apparent change is explained by the relative motions of the different basic atoms. Plato was influenced by all of these. But I would say the theory of forms accounts more for constancy or regularity more than change, no?
Btw, the central concept of Parmenides' philosophy is always translated as "Being", but I couldn't find the original Greek word. It isn't "ousia"?
I'm not sure about Plato, but the Aristotelian analysis is something like this: every thing that exists has the potential to exist in certain ways and not others, and it's said that the thing is "in potency" to exist in those potential ways. When something could exist in a certain way but right now doesn't, that's called a "privation." And the ways that the thing currently does exist are the "form" of the thing. So a substance changes when it goes from being in potency to being actual, and it does that by losing a privation. Aquinas follows Aristotle in giving the example: "For example, when a statue is made from bronze, the bronze which is in potency to the form of the statue is the matter; the shapeless or undisposed something is the privation; and the shape because of which it is called a statue is the form." Incidentally, Aquinas's short On the Principles of Nature (https://aquinas.cc/la/en/~DePrinNat) is a good overview of this theory, which is spread all over Aristotle (in the Categories, the Physics, and the Metaphysics).
As far as οὐσία is concerned, I think this is the complete Greek for Parmenides's poem: http://philoctetes.free.fr/parmenidesunicode.htm. In the places where that translation uses "being" you get slightly different words like γενέσθαι (to come into a new state of being) or εἶναι (just the infinitive "to be"). And looking at the definition of οὐσία (https://lsj.gr/wiki/%CE%BF%E1%BD%90%CF%83%CE%AF%CE%B1) it looks like most of the uses of that term specifically come well after Parmenides.
https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...
This is a golden quote.
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_.
But when authors start slinging around Plato and Aristotle and especially Parmenides willy-nilly alongside modern principles, they're waving a red flag... Don't get me started!
Well, that's not true.
Particles, and thus facts, pop into and out of existence all the time.
> We know that two orders are isomorphic if there are two functors, such that going from one to the other and back again leads you to the same object.
And I have no clue what is a functor, nor order. "Functor" wasn't defined, and "order" is defined as "thin category", which in turn remains undefined.
Seems to me like in order to understand this text you already need to understand category theory. If that's the case, then why would you be reading it?
Get off my lawn! And start giving things long descriptive names that are aliased to acronyms again! db2, netcat, socat, emacs (editing macros), wget...etc.
If you press the Prev button at the top of the page it takes you back to Functors. Twice more and it will take you back to Orders.
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 category theory you can specify that two mappings be equal and you can also specify that two mappings compose end to end to produce a third mapping.
Category theory can be used to express some requirements in a very concise way.
I'm not sure about that, because you still need some concept of set (or collection or class) to define a category, because you need a set of objects and mappings between them (technically that's a "small" category, but to define any larger category would require at least as much set-theoretical complication).
More exactly, whereas in set theory it's the membership relation between sets and their elements that is basic, in category theory it's the mapping between objects.
Nevertheless, the basic concepts of set theory can also be defined within category theory, so in that sense they're inter-translatable. In each case though, you need some ambient idea of a collection (or class or set) of the basic objects. Tom Leinster has a brilliantly clear and succinct (8 pages) exposition of how this is done here https://arxiv.org/abs/1212.6543
The thing is, even defining first-order logic requires a (potentially infinite) collection of variables and constant terms; and set theory is embedded in first-order logic, so both set theory and category theory are on the same footing in seemingly requiring a prior conception of some kind of potentially infinite "collection". To be honest I'm a bit puzzled as to how that works logically
Two mappings with corresponding domain/codomain have to compose by definition of a category. It's not something you can specify.
Could you give an example in programming, what can be easier expressed in CT than with sets and functions?
Why have I never seen it explained like this before. Wow, thank you!
Can you an example?
I decided to look for other cases where this process worked.
I found several, but one off the top of my head is high dimensional analysis, where t-SNE was doing okay, and a group decided to start with CT and try to build something better, and produced UMAP, which is much better.
In short, this does work, and you can find much better solutions this way.
(random link https://stats.stackexchange.com/questions/402668/intuitive-e... )
... because mappings map nicely to functions
At the same time, it's actually rather more accessible than most other areas of pure math—at least at the level that people talk about it online. Basic category theory can be hard to learn because it's so abstract but, unlike almost any other are of math from the 20th century onwards, it has almost no hard prerequisites. You can reasonably learn about categories, functors, natural transformations and so on without needing a graduate degree's worth of math courses first. You might not understand the most common examples mathematicians use to illustrate category theory ideas—but it's such a general framework that it isn't hard to find alternate examples from computer science or physics or whatever else you already know. In fact, I expect most of the articles that get talked about here do exactly that: illustrate category theory ideas with CS/programming examples that folks on HN find relevant and accessible.
This is the whole premise of _Conceptual Mathematics_: category theory for high school students.
Category Theory's approach of "don't do any introspection on the elements of the set" led it to focus on some structures that turned out to be particularly common and useful (functors, natural transformations, lenses, monads, etc.). Learning these is like learning about a new interface/protocol/API you can use/implement - it lets you write less code, use out-of-the-box tools, makes your code more general, and people can know how to use it without reading as much documentation.
Focusing on these also suggests a generally useful way to approach problems/structuring your code - rather than immediately introspecting your input and picking away at it, instead think about the structual patterns of the computation, and how you could model parts of it as transformations between different data structures/instances of well-known patterns.
As a down-to-earth example, if you need to schedule a bunch of work with some dependencies, rather than diving into hacking out a while-loop with a stack, instead model it as a DAG, decide on an order to traverse it (transform to a list), and define an `execute` function (fold/reduce). This means just importing a graph library (or just programming to an interface that the graph library implements) instead of spending your day debugging. People generally associate FP with recursion, but the preferred approach is to factor out the control flow entirely; CT suggests doing that by breaking it down into transformations between data structures/representations. It's hugely powerful, though you can also imagine that someone who's never seen a DAG might now be confused why you're importing a graph library in your code for running async jobs.
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.
as a very broad example there are multiple ways to define a “homology” (ex simplicial, singular, etc) functor associating certain groups to topological spaces as invariants. but the arguments needed to prove properties of the relationships between those groups can be derived from very general properties of the definitions and don’t need to be re-argued from the very fine definitions of each type of homology.
i think.
In computing, we think about:
- a set of states
- with transformations between them
- including a ‘do nothing’ transformation
- that can be composed associatively (a sequence of statements `{a; b;}; c` transforms the state in the same way as a sequence of statements `a; {b; c;}`)
- but only in certain ways: some states are unreachable from other states
This is exactly the sort of thing category theory studies, so there's a lot of cross-pollination between the disciplines. Computation defines interesting properties of certain categories like ‘computation’ or ‘polynomial efficiency’ that can help category theorists track down interesting beasts to study in category theory and other branches of mathematics that have their own relationships to category theory. Meanwhile, category theory can give suggestions to computer science both about what sort of things the states and transformations can mean and also what the consequences are of defining them in different ways, i.e. how we can capture more expressive power or efficiency without straying too far from the comfort of our ‘do this then do that’ mental model.
This latter is really helpful in computer science, especially in programming language or API design, because in general it's a really hard problem to say, given a particular set of basic building blocks, what properties they'll have when combined in all the possible ways. Results in category theory usually look like that: given a set of building blocks of a particular form, you will always be able to compose them in such a way that the result has a desired property; or, no matter how they're combined, the result will never have a particular undesired property.
As an aside, it's common in a certain computer science subculture (mostly the one that likes category theory) to talk about computing in the language of typed functional programming, but if you don't already have a deep understanding of how functional programming represents computation this can hide the forest behind the trees: when a functional programmer says ‘type’ or ‘typing context’ you can think about sets of potential (sub)states of the computer.
> - with transformations between them
>
> - including a ‘do nothing’ transformation
>
> - that can be composed associatively (a sequence of statements `{a; b;}; c` transforms the state in the same way as a sequence of statements `a; {b; c;}`)
I mean, all examples I heard can be directly treated with groups, monoids, and regular functions.
I know some abstract concepts that can be defined in a nice way with CT but not nearly as easy - set theory, e.g. (abstract) tensor product. Yet, for other concepts, including quantum mechanics, I have found that there is "abstract overhead" of CT with little added value.
IMO a better reply would be: category theory appeared to unify the concepts around using discrete objects to prove the properties of continous objects in topology, like fundamental groups, homology groups and homothopy groups. It is only practically useful for very advanced proofs like 2nd Weil Conjecture. Any usage of it in programming is only an analogy and is not mathematically rigorous (see https://math.andrej.com/2016/08/06/hask-is-not-a-category/)
Thanks for the Parmenides poem. It seems much more straightforward than the various commentaries and analyses I've seen written about it.
VIII.16: ἔστιν ἢ οὐκ ἔστιν· :: It is or it is not
Very nearly "to be or not to be"...
For more detail, see Bartosz Milewski, Category Theory for Programmers:
"Composition is at the very root of category theory — it’s part of the definition of the category itself. And I will argue strongly that composition is the essence of programming. We’ve been composing things forever, long before some great engineer came up with the idea of a subroutine. Some time ago the principles of structured programming revolutionized programming because they made blocks of code composable. Then came object oriented programming, which is all about composing objects. Functional programming is not only about composing functions and algebraic data structures — it makes concurrency composable — something that’s virtually impossible with other programming paradigms."
https://bartoszmilewski.com/2014/10/28/category-theory-for-p...
i;a = a
Now, if there is another mapping j that is different from i, such that
j;a = a
If there is no such j then mapping a is said to be a monomorphism or injection (the set theoretic term) and it does not lose information.
This specification of the property 'loses information' only involves mapping equality and mapping composition. It does not involve sets or elements of sets.
An example of a mapping that loses information would be the capitalization of strings of letters. An example of a mapping that you would not want to lose information would be zip file compression.
If you alter the above specification to use post-composition (a;i = a and a;j = a) instead of pre-composition you get epimorphisms or surjections which capture the idea that a mapping constrains all the values in its codomain. I like to think of this as the mapping does not return uninitialized values or 'junk' as it is sometimes called.
Bartosz Milewski works through this in more detail (including from the set-theoretic side) in the last 10 minutes of https://www.youtube.com/watch?v=O2lZkr-aAqk&list=PLbgaMIhjbm... and the first 10 minutes of https://www.youtube.com/watch?v=NcT7CGPICzo&list=PLbgaMIhjbm....
If all you know is that you have two mappings you don't know they compose, until you get the additional information about their sources and targets. In a way that's what the source and targets are: just labels of what you can compose them with.
CT is more of a way to abstract all mathematics.
Allowing uncountably many symbols can be more convenient when you apply logic in other ways, e.g. when doing model theory, but from a foundational perspective when you're doing stuff like that you're not using the "base" logic but rather using the formalized version of logic that you can define within the set theory that you defined using the base logic.
I don't think you need set theory to define set theory (someone would have noticed that kind of circularity), but there still seems to be some sleight of hand in the usual presentations, with authors often saying in the definition of first-order logic prior to defining set theory that "there is an infinite set of variables". Then they define a membership relation, an empty set, and then "construct the natural numbers"... But I guess that's just a sloppiness or different concern in the particular presentation, and the seeming circularity is eliminable.
Maybe instead of saying at the outset that we require natural numbers, wouldn't it be enough to give an operation or algorithm which can be repeated indefinitely many times to give new symbols? This is effectively what you're illustrating with the x, x*, x**, etc.
If that's all we need then it seems perfectly clear, but this kind of operational or algorithmic aspect of the foundation of logic and mathematics isn't usually acknowledged, or at least the usual presentation don't put it in this way, so I'm wondering if there's some inadequacy or incompleteness about it.*
I think the argument I presented above adequately justifies CT as fundamentally connected to computation, at least as we study it today, though I think there are other formalisms as well that are just as worthy.
> CT is not a recognized Computer Science subject
I'm not sure who decides this :) Certainly when I studied computer science we had modules on category theory, along with other applicable ‘discrete math’ subjects.
CS is a bit of a grab-bag of a discipline, so it's very hard to say what does or doesn't belong on a CS curriculum. But I think programming language semantics, which is the field where you see CT pop up the most, is probably uncontroversially CS, or at least I don't know what other discipline would claim it.
> It's mostly used in the functional programming community to name certain concepts and theorems
It's mostly used in the PL community; its use in functional programming is an attempt to connect the language more directly to that lineage (or because functional programming languages traditionally came from that community, where the language is already understood and available to describe things).
> but then applied to a specific type system (so it's not actually doing CT, since your restricting yourself to a single category, whereas CT is really about connecting different categories by generalizing over them)
I agree that there's not a lot of interesting category theory to do when restricted to a single category, but this isn't quite correct. Some type systems, e.g. simply typed lambda calculus, are adequately _described_ by a single category, though in more advanced cases you usually need more than one (e.g. dependently typed languages are often described by ‘categories with families’, which are a slightly more sophisticated category-theoretical construction). But even within a single type system you usually find many categories; for example a type system can often be described by a category of terms that map between its typing contexts, but within that category you also have a category of types and functions between them, a category of (functorial) type constructors and natural transformations, et cetera. An important family of examples are the Kleisli categories over monads: every monad actually defines a category of its own, whose categorical laws give the good behaviour of monads that make them useful for composing effectful computations. Interactions between these different categories are where inspiration comes from for CT-flavoured API design, e.g. the ‘interpreter’ pattern that's popular in Haskell (https://softwareengineering.stackexchange.com/questions/2427...). Even in pure CT the study of ‘connecting different categories’ can be seen mostly as taking a sufficiently close look at the category `Cat` of categories and functors!
Upon careful inspection or after just writing/using them 10,000s of times[1] you realize they are both special cases of one general function f()[2]. Congrats, you're likely doing CT now, but barely scratching the surface, though.
Let's say you find a way to do a function factory that generates explicit instances of f() -> A() and f() -> B() at runtime for your different use cases as they are needed. You do this 100 times, 1,000 times[1] with many different functions, in many different contexts. You eventually realize that if all your functions and their signatures had the same structure[3] it would be quite easy to mix some (or all?) of them with each other, allowing you to handle a perhaps infinite amount of complexity in a way that's very clean to conceptualize and visualize. Isn't this just FP? Yes, they're very intimately related.
By this point you're 99.9999% doing CT now, but remember to shower regularly, touch grass etc.
CT formalized these structures with mathematical language, and it turns out that this line of thinking is very useful in many fields like ours (CS), Math, Physics, etc.
1. Which is what happened to me.
2. Which sometimes is a way more elegant and simple solution.
3. This term is fundamental and has way more meaning than what I could write here and what one would think on a first approach to it.
If you have a working intuition for categories then in most cases the specific formulation you choose as a foundation doesn't matter, just as most mathematicians work nominally in set theory without worrying about the subtleties of ZFC.
From a programming perspective, though, a fair few important things have (by now) turned out to be useful that have come as a result of rephrasing programming in mathematical terms. Some top contenders are monads (directly from CT — think Haskell, but also LINQ, JavaScript Thenables, async/await, Rust Option/Result combinators, parser combinators), proof assistants and modern approaches to type systems, linear/substructural logic (think Rust or C++ move semantics), functional programming (which is now embraced at least to some extent by all mainstream programming languages), functional reactive programming (the core ideas behind things like React), et cetera.