Programming with Categories(brendanfong.com) |
Programming with Categories(brendanfong.com) |
What is the beautiful monospace font in the pdf here http://brendanfong.com/programmingcats_files/cats4progs-DRAF...?
OMG. That might just be the funniest god-damned thing I've ever seen in my life. Thanks for sharing that!
On a separate note: does anyone know where this footage is originally from? Some WWII movie, I would guess?
Probably one of the best "WWII movies" (it's really only about the final days in the bunker) ever.
Jokes aside, a book like CTM shows both paradigms have their place, and can also co-exist in the same system.
Besides, this paper cleared all my doubts about high-order FP having a lot of (unexploited) potential:
This made me laugh way more than it should have. "Why don't you pattern match my fist all over your faces!"
And the last line....
Alright, maybe I will keep reading this book.
t1xtt, from the txfonts package, freely available
Hitler: What's a monad anyway? No one who understands monads can explain what they are
Underling (hurriedly): A monad is just a monoid in the category of endofunctors
A helpful analogy can be drawn by comparing two facts: a composition of something with its inverse produces the identity (a.k.a. unity, to use the Latin root), while a composition of something (e.g. a functor) with its "adjoint" (not quite the inverse) produces something similar that is better said in Greek.
Gotta be able to laugh at yourself sometimes.
When previously taught, people would remain afterwards to ask questions, discuss math, and chat. So this was an iterative-improvement formalization of that.
People would gather in front of the blackboards in fluid discussion clusters. Catalyzed by the three instructors and wizzy others, not all having to stay for the entire hour, but drifting off as discussion died away. They could show material they had pruned from the lecture, for want of time. Or got dropped as they ran over. Alternate presentation approaches they had considered, before selecting another. They could be much more interactive. One commented roughly "If I was tutoring someone, I'd never present the material this way". It was a delightful mix of catching the speaker after a talk to ask questions, a professor's office hours, a math major's lounge, an after-talk social, tutoring, an active-learning inverted classroom, hanging out with neighbors in front of the hallway blackboard, chalk clattering and cellphones clicking to snag key insights... It was very very nifty.
So, the book is nice. And lecture notes. And videos. But... the best part isn't there. Perhaps the next iterative improvement is to capture the aftermath on video, and share that too.
And as we look ahead, planning distance-learning and XR tools... maybe something like this is a vision to aspire too. The insane ratio of expertise to people learning is not something one can plausibly replicate in meatspace. But as conversations in front a virtual blackboard gradually become technically feasible, something like this might pay for the cost of it, with transformative impact.
Why are you paying for that nonsense?
https://github.com/zio/zio-prelude
It's a brand new library for Scala that contains reusable mathematical structures. Still based on algebra and category theory, but it expresses them more or less differently than how they've been expressed in Haskell (and similar languages). For example, unlike Haskell (and Scala's own cats and ScalaZ), it doesn't present the "traditional" Functor -> Applicative -> Monad hierarchy. Instead, it presents the mathematical concepts in a more orthogonal and composable way.
One example out of many, you don't have a Monad. You have two distinct structures:
* Covariant functor, with typical map operation `map[A, B](f: A => B): F[A] => F[B]`
* IdentityFlatten which has a flatten operation `flatten[A](ffa: F[F[A]]): F[A]` and an identity element `any: F[Any]`
When combined together (Scala has intersection types), you get something equivalent to the traditional Monad.
The project is in its infancy, so it may still change significantly, though. Look here for more detailed explanation:
https://www.slideshare.net/jdegoes/refactoring-functional-ty...
Btw, this is a problem that the "Selective applicative functor" too aims to alleviate.
You can read more about the inspectability problem (and Selective) at http://eed3si9n.com/selective-functor-in-sbt
The context there is sbt, which is a build tool, but I'm sure the inspectability plays role in many other areas. Note, how he contrasts "Applicative composition" and "Monadic composition".
And yet, the current mathematics relies heavily on the ZFC set theory. Why is that ? (Is that assumption even correct ?)
From what I've learned so far, the set theory suffers from Russel's Paradox[0] (does the set of all sets that does not contain itself, contains itself ?). That's what motivated the formalization of Type Theory and the invention of Type Systems in programming languages.
According to wikipedia[1], some type theories can serve as an alternative to set theory as a foundation of mathematics.
It seems to me that the Category Theory fits the description. So why don't we see a huge "adoption" in math fields ?
Thank you in advance for your clarifications :)
[0] - https://en.wikipedia.org/wiki/Russell%27s_paradox [1] - https://en.wikipedia.org/wiki/Type_theory
This is a fantastic "side effect" of the fact that category theory isn't built on any other mathematical knowledge. You don't even need even any arithmetics for that.
Pretty wild ideas, though. Fair chance they'd be more confusing than using more specifically named instances, but solid ideas where the class instance documents that you're using the pattern, instead of describing the preferred interface.
I suppose it might help sometimes when designing an abstraction, to guide you to some nice properties, such as easy composition.
You can write monoid and foldable interfaces in java but in haskell finding the head of a list with a monoid and foldmap is constant time (and the first or last element of a tree is logarithmic) but a java implementation would be linear.
If you haven't read it, take a minute...
Category Theory could be the rosetta stone of many things(this is relevant https://arxiv.org/pdf/0903.0340.pdf).
[0]https://www.azimuthproject.org/azimuth/show/John+Baez [1]https://forum.azimuthproject.org/discussion/1717/welcome-to-... [2]http://math.mit.edu/~dspivak/teaching/sp18/7Sketches.pdf
You are going to have to revive jesus to come up with a functional language that simplifies coding over a procedural one. Especially over an object oriented one.
There are people working on categorical foundations, but the main reason for lack of broader popularity or drive is that most mathematicians don’t do work that is “foundational” in that sense. For example, if you’re an analyst, you generally don’t care exactly how your real numbers are built (dedekind cuts, Cauchy sequences, etc.). You only care that they satisfy a certain set of properties, you can define functions between them, and that’s about it. Most mathematical reasoning at this level is insensitive to differences in proposed foundations, except “constructive” foundations that don’t have the law of excluded middle (that are unpopular since they make many proofs harder and some impossible).
What is very popular in mathematics is using category theory at a high level; basically every field uses its concepts and notation to some degree at this point. New foundations are only really relevant to this program in that they may make automated proof checking easier, which is also not a widespread practice in mathematics.
In fact, I would suggest that most mathematicians don't care about category theory at all.
The thing to keep in mind is that a mathematical structure can be expressed as instance of any number of more general mathematical structures ("mathematical machinery"). The structures that useful, however, are those that are "illuminating", a somewhat vague criteria but one which generally include a structure facilitates and unifies proofs of important theorems. Wiles' proof of Fermat's Last Theorem showed the value of many forms of this mathematical machinery [1], including category theory.
At the same time, I think things like Godel theory of cutting down proofs and Chaitin's Omega constant give a suggestion that the some number of "important" theories within a given axiomatic system will have long proofs that don't necessarily benefit from the application of a given piece of mathematical machinery, whatever that machinery.
And think that's related to efforts to apply category theory to programming via functional programming. I feel like it's an effective method for certain kinds of problems but that you get a certain problematic "it's the best for everything" evangelism that doesn't ultimately do the approach favors.
[1] https://en.wikipedia.org/wiki/Wiles%27s_proof_of_Fermat%27s_...
So-called "naive set theory" does, but my understanding is that this paradox (and others like it) sparked a crisis in mathematics that led to the creation of ZFC and others. ZFC is not known to be inconsistent (due to deep and technical reasons, I can't claim positively that it is consistent), and it was designed to avoid the paradoxes that plagued naive set theory.
Russell's type theory was another early contender for a formalism. For whatever reason (I'm not aware of all the details), Zermelo-Fraenkel set theory (later extended with the Axiom of Choice) won the popular mindshare. Personally, I'm more a fan of the Elementary Theory of the Category of Sets (ETCS) [1], which is indeed drawn from category theory. But it's equivalent in deductive power to ZFC, so what you pick mostly only matters if you're doing reverse mathematics. (This is what really answers your question, I think.)
Russell's type theory and modern type theories are distinct (and there is no single "type theory"). I'm led to believe the commonality is primarily with the usage of a hierarchy of universes, so that entities in one unverse can only refer to entities in a lower universe.
[1] "Rethinking set theory", Tom Leinster: https://arxiv.org/abs/1212.6543
That was my understanding as well. Axiomatic Set Theory, with ZFC, doesn't suffer from the same problems as Naive Set Theory, which is why it was developed. Or so I've read.
Set theory is the de facto modern standard because it has straightforward notation and sufficient power to prove the things most mathematicians care about, both algebraically and analytically. Other foundations exist, it's just that most mathematicians work at a level where set theory is more of a communication and notation tool than a foundation for which the nuances matter.
> From what I've learned so far, the set theory suffers from Russel's Paradox[0] (does the set of all sets that does not contain itself, contains itself ?).
No, naive set theory suffers from Russell's Paradox, but ZFC does not. ZFC was defined in order to avoid Russell's Paradox.
> That's what motivated the formalization of Type Theory and the invention of Type Systems in programming languages.
Russell's type theory, yes, which predates ZFC. But this has nothing to do with programming languages, which weren't a thing when this problem was being considered.
As for why category theory isn't used as a foundation - that's not really what category theory's "charter" is about. As user johncolanduoni explained, category theory is more of a framework for describing things with convenient algebraic abstractions than it is a foundation for mathematics. Category theory as practiced today is mostly done at a higher level than the foundational set theory.
1. I thought mathematics was moving more towards a category theory based foundation, as opposed to the set theoretical stuff.
2. Isn't it in part because we have over 120 years of results and proofs that are based on set theory, and people aren't just going to throw that out for something newer? Granted, Category Theory has been around in some form since about the 1940's, but it's still newer than set theory.
3. Russell's Paradox hasn't stopped people from using Set Theory to achieve useful results, and the axiomatization of Set Theory and the advent of ZFC is why (or at least part of why) that was possible, no?
2. ZFC is fully adequate for all the mathematics 99% of professional mathematicians do (and probably more than adequate in terms of strength). Also, all the mathematics 99% of mathematicians do is insensitive to foundational issues, so if you swapped ZFC for another axiomatization of similar strength, no one would notice.
3. I don't believe ZFC was the first to avoid the paradox, but yes, it does not suffer from Russell's Paradox.
Because most math fields work at a higher level, and whether they consider set theory or category theory foundational doesn't matter. For instance, the defining property of ordered pairs is: `(a, b) = (c, d) iff a = c and b = d`. {a, {a,b}} is a (set-theoretic) model for ordered pairs, but it's not the only model. As long as a model exists, the question of "which model you're using" isn't relevant.
Not really. Most working mathematics is done without any particular foundational context (in fact, it's probably done in naive set theory). If you asked a mathematician, they'd tell you they were using ZFC, but only because everyone does; in practice they don't know or care what foundations they're working with.
> From what I've learned so far, the set theory suffers from Russel's Paradox[0] (does the set of all sets that does not contain itself, contains itself ?). That's what motivated the formalization of Type Theory and the invention of Type Systems in programming languages.
Naive set theory suffers from that paradox. ZFC is a minimal "patch" that avoids it (through the rather ugly hack of an axiom schema).
It shouldn't surprise any programmer that most people working in the field would rather use a bodge that lets them use all their existing theorems and avoid having to learn anything new, rather than a new foundational paradigm.
People who care deeply about foundations are working on things like HoTT. But it's just not that important to day-to-day working mathematicians.
ZFC is a bit messy sometimes, but it's actually kind of nice in its simplicity. I am a big fan of TLA+, for example, and it's really kind of beautiful how easily you can define incredibly precise invariants by using the set theory predicate logic.
This is purely secondhand, of course, and I forget almost all of the details. Contemporary set theory is scary scary stuff.
(Of course there is a lot of stuff in set theory that is counter-intuitive when you get to infinite sets, but I still think that's better than what you have with categories where they're just abstract algebraic objects and there isn't any intuition in the first place.)
It's true that you can get away from Russell's paradox in category theory, but that's because categories are not sets and have different properties (there's less you can say about them because they're more general).
Type theories, particularly homotopy type theory, are becoming popular among some mathematicians, but not because they escape Russell's paradox (I'm not sure that they can say anything more about sets than set theory), but because they are more useful when constructing automated proof systems.
Edit: also, category theory is used a lot in very cutting edge math, like algebraic topology.
I don't think that's right. The original invention of type systems in programming had nothing to do with Type Theory. The motivation wasn't from any theory. The point was to tell Fortran whether to treat a value as an integer or a floating-point number, which affected storage format and a bunch of other things. (Before Fortran, there was floating-point arithmetic, but the type was still just a computer word. The programmer had to keep track of what format it was in.)
> It is easy to establish this result for polygons, but the problem came in generalizing it to all kinds of badly behaved curves, which include nowhere differentiable curves, such as the Koch snowflake and other fractal curves, or even a Jordan curve of positive area constructed by Osgood (1903).
So to some extent, the reason why such an "obvious" statement requires a complicated proof is because our everyday notions of what a "closed curve" is are much more restricted than what we consider in mathematics. This is kind of common in maths, especially in fields with a lot of visual intuition.
So, in addition to being able to raise numbers to powers I could also use it on matrices whose elements belonged to a semiring.
That is, I could use the same code on a matrix of doubles with "times" and "plus" (for the Markov chains), as well as a matrix of booleans with "and" and "or" (for the graph connectivity).
(Of course, I could have used special purpose libraries, but these were small problems and it was fun. :)
At least in Haskell one thing it means is you can use lots of new helper functions.
> guide you to some nice properties, such as easy composition.
Yep, which gets you code re-use for one.
That's what the recent CALM Theorem [1] paper uses as the first theorem:
> Monotonicity is the key property underlying the need for coordination to establish consistency, as captured in the CALM Theorem:
> THEOREM 1. Consistency As Logical Monotonicity (CALM). A problem has a consistent, coordination-free distributed implementation if and only if it is monotonic.
Unsurprisingly, this paper is reference 32 in CALM. Maybe I should check out some other papers referenced here... Thanks for the recommendation!
[1]: https://cacm.acm.org/magazines/2020/9/246941-keeping-calm/fu...
(And to be fair, half of them are the same overused ones. But the others are good.)
There is often an undercurrent of category theory within a subject that maybe most people are not privy to. Anything to do with sheaves or cohomology (which I know factors into some approaches to PDEs) are using categorical ideas.
Every generation, it seems, has some contingent of serious mathematicians who consider category theory marginal in their field of interest. But every generation, that contingent grows smaller as more mathematics as practiced is brought into the fold. Maybe they're coming for you next :)
Whether combinatorialists ought to elevate certain work is of course of a question of value, but it's also a different question.
Also, in no way are sheaves or (co)homology essentially category-theoretic ideas. It's possible to develop and use these ideas without mentioning categories at all (and e.g. Hatcher's introductory textbook does just this, although he mentions in an appendix the categorical perspective later). In general I think it's good to remember that homological algebra and category theory are not the same subject. Sure, I can develop a theory of chain complexes over an arbitrary abelian category, but most of the time you just need Hom and Tor over a ring. (Again, see Hatcher.)
Finally, I'm not sure there has been a serious uptake in category theory in the mainstream of some field of mathematics since, I don't know, at least 50 years ago? We've understood for a while now what it's good and not good for. This hasn't stopped people from trying to inject it in fields where it doesn't do any good (e.g. probability), but for that reason those attempts are mostly ignored.
I think it is also a reasonable interpretation to take "mainstream" as "pertaining to the main subject matter of the field". Anyway, I think it is the case that the mainstream of combinatorics or probability is yet so big that a particular researcher or even group of researchers can be comfortably in the mainstream and yet have never cared for or even heard of some other line of research that is also mainstream.
The founding paper of combinatorial species [1] has hundreds of citations including many in what I gather are top journals in combinatorics, and even some in the Annals of Probability. So, what are we to make of that? Some people who are serious enough about combinatorics or probability to get published in serious journals have read, perhaps understood, and maybe even taken seriously some of these categorical ideas?
In any case, I respect your viewpoint. In my youth I was a bit category-crazy, trying to use it to organize all of my mathematical knowledge. I'm much more prudent about it these days but I'm still an optimist that we will find more unifying ideas in mathematics through it.
[1] https://www.sciencedirect.com/science/article/pii/0001870881...
Agree, but only on the level on which they do not care about the abstract math (algebra, topology, etc.) in general. As soon as you step into the territory of the abstract math, especially where different disciplines blend, such as homology and cohomology, category theory (and its diagram language) helps a lot to clarify things. (Incidentally, a lot of this stuff is now part of the "applied math" as well, having found its way into theoretical physics, for example.)
I also am reluctant to characterize theoretical physics as "applied math." I haven't seen anyone who calls themselves an applied mathematician use category theory in a substantive way (where here I am thinking about numerical computing, mathematical biology, and so on).
“How much salt should I add?”
“Oh, not too much.”
Practically guarantees a withering glare from me.
I admit it's kind of frustrating that it can't be boiled down to a list of discrete things you need to know, but if I had to explain the difference between me before I had "sufficient mathematical maturity" and me after, I would explain it in terms of habit and confidence and other squishy things that aren't mathematical at all.
Most pizza dough recipes quote around 5g of salt for 250g flour. Personally I prefer double that amount, and this is the case with many recipes.
Perhaps specifically with salt there is an insane amount of paranoia about blood pressure. In many ways it feels as irrational as Korean worries about fan death.
On the other hand, giving a "5g of salt" value is a good starting point, to avoid undersalting due to paranoia or oversalting due to inexperience.
That said, a background in mathematics helps with category theory. Things like group theory, topology (particularly algebraic topology), Galois theory and set theory can be useful in motivating a lot of category theory. I’m yet to see much of a strong motivation from programming (where is there a functor that isn’t an endofunctor?)
Over time it has fallen away in two directions.
In one direction is that though you are always stuck in a category with types as objects and functions as arrows, that doesn't stop you from subdividing. This became more intuitive to me as I encountered more and more categories that are basically just Set with extra structure (just as the one we program in is basically Set with bottom). If you start putting extra structure on your arrows (that is something that carries around a function along with some extra proof-relevant structures, like say a way to show that some zero element in the domain under the function equals the zero element in the codomain and that multiplication is preserved under the function, now you have monoid-homomorphisms) then you end up in the general case with something that looks a lot like a binatural transformation of profunctors, which pretty cleanly encodes "exo"-functors between different sub-categories of the category with all types as objects and functions as arrows.
In the other direction is realizing that even imprecisely, there's quantifiable value in observing functors to and from the category of types and functions, say one between whiteboard diagrams and code, or between a specific problem domain and code, etc etc. If you have some other space with composable relationships that you want to preserve when you write code to correspond to it, or you have some other representation you want to produce based off some given codebase while preserving the structure of the code taken as input, you can gain a ton of conceptual leverage out of identifying a functor.
Endofunctor: A -> A, for category A
Functor: A -> B, for categories A and B
Edit: A piece of advice that has stuck with me for a long time, long after I forgot where it came from, is it's a mistake to look for the state in between "not salty enough" and "too salty." That state doesn't really exist, especially when you're feeling nervous! Instead you should look for the overlap where you can perceive the dish as alternately "not salty enough" and "too salty," like that ambiguous drawing that your brain can resolve to either an old woman or a young woman[0]. That advice really works for me, but my wife, who seasons like a pro, thinks it's nonsense, which I think illustrates how subjective the process is and how it isn't information you can impart but rather experience you have to guide someone toward.
[0] https://en.wikipedia.org/wiki/My_Wife_and_My_Mother-in-Law#/...
Regarding your claim about that paper being cited by papers in top journals, I checked the first five pages of citations in Google Scholar for combinatorics and probability journal papers.
It's cited once in an offhand way in the concluding discussion of "The Cycle Structure of Random Permutations." No categorical concepts are used there. Ditto for the "Independent process approximations" paper (except now cited in the introduction). Another one-sentence mention in the context of background literature appears in "Tree-valued Markov chains derived from Galton-Watson processes." Same for "A Combinatorial Proof of the Multivariable Lagrange Inversion Formula" and "Bijections for Cayley Trees, Spanning Trees, and Their g-Analogues."
There's a one-sentence mention with actual (slight) mathematical content in "Limit Distributions and Random Trees Derived from the Birthday Problem with Unequal Probabilities." But you don't need categories to prove the bijection they're referring to, from what I understand.
In none of these instances is the work used in a substantive fashion, and unless I missed something no paper features the word "category." It's getting cited because authors have a duty to survey any potentially related background literature.
(On page 6 I found "Commutative combinatorial Hopf algebras," which does use a functor form that paper. It was published in a journal that is decent, but very far from the top.)
So, I think we can reject the notion that Joyal's paper has seriously influenced the fields of combinatorics or probability.
I'm sorry to harp on this, but I see claims like yours about the importance of category theory thrown around a lot on here, and often I feel that they're clearly wrong. So I thought it would be good to provide some details this time around.
I pick these two papers. The first is literally about adjunctions pertaining to combinatorial species whereas the second devotes an entire section to reviewing the theory and stating results that it uses in a way that I don't really understand. I'm going to read the first paper though because it's relevant to my interests :)
Rajan. The adjoints to the derivative functor on species
https://www.sciencedirect.com/science/article/pii/0097316593...
Panagiotou, Konstantinos; Stufler, Benedikt; Weller, Kerstin. Scaling limits of random graphs from subcritical classes.
https://projecteuclid.org/euclid.aop/1474462098
The fact that I have to go rummaging around for these examples kind of proves your point, doesn't it? I don't think category theory will lead to any fantastic new results in the fields we're discussing, but the bar is quite low for it to be useful as an organizational tool.
^ I searched for the word functor of course! :)
The second paper is interesting because it's in an excellent journal and about a problem not obviously connected with species. So I agree that it counts as a good example for your case. I also agree with your conclusion – it's an exception that proves the rule, so to speak. Most probabilists have no need for category theory, and most AoP papers don't use categories. (I feel that may literally be the only one?)
I also agree that, to the extent it's useful, it's useful as an organizing principle and not "substantively." I suppose this explains why I feel it's overhyped: mathematicians care about solving problems, and the insights that solve the problems ultimately have to come from some problem-specific observations.
In particular, a map between categories that does not preserve composition is not a functor. It is important that F(f;g) = F(f);F(g).
It feels like doing “group theory” entirely with the symmetric group of the integers. While it’s true that the group is very general and has interesting properties, the focus of group theory isn’t single groups but rather the relationships between groups.
Compare this to something like algebraic topology or Galois theory where you have a Galois correspondence (a functor) between objects you’re interested in and groups.
