Am I missing something or did the anecdote at the beginning have nothing to do with the rest?
265 karma · joined February 1, 2014
Blaming everything on "entitlement" from people who bought Elm's marketing about "making functional programming practical" is ridiculous. Thankfully there are now plenty of languages with better type systems than Elm (Rust, OCaml) that deploy to the web just fine.
And certainly from an abstraction point of view you can do this in any dependently typed language like Idris/Agda/Coq, but these don't have great implementations.
This is a very interesting question and I think reflects a mismatch between how we commonly think about of foundations of mathematics and what role foundations actually play in mathematics. There's no recording online but I recommend looking at the slides to Mike Shulman's talk from JMM 2022 where he discusses this point: http://sigmaa.maa.org/pom/Slides/shulman-2022jmm.pdf . Mike works on, among other things, homotopy type theory, the subject of the original article.
His basic point is that we should think of math more like programs that we can "compile" to various backends. If your math is high level it's not necessarily tied to a particular "architecture" like ZFC.
The "big" theorem of basic category theory is probably the adjoint functor theorems which, once you realize that so many constructions in math are adjoint functors, gives very useful technical conditions to construct such an adjoint (ctrl-s for "applications" here for examples: https://math.stackexchange.com/questions/844131/adjoint-func...).
The most delightful surprising results to me come from categorical logic because that is what I am most familiar with. Here is one: any elementary topos is a model of intuitionistic higher-order logic, and also extensional dependent type theory. This vastly expands the domain of applications of logic if you are used to thinking only in terms of set-theoretic models. It also gives us applications of constructivism that are entirely independent from any philosophical debate about the nature of truth. This means that you can take many mathematical fields such as differential geometry, algebraic geometry, topology, as embodied in some category C, embed them into a sheaf topos and then use intuitionistic logic to do constructions and theorems in this area that are vastly simpler than the usual formulations. For instance you can do this with differential geometry and get an intuitionistic logic where you can work explicitly with infinitesimal numbers to calculate derivatives in a completely rigorous fashion. Ingo Blechschmidt has written some expository material in this vein (his main work being in using this in algebraic geometry): https://arxiv.org/abs/2204.00948
On the "surprising" side, I think the most surprising things for me where seeing how existing mathematical structures were examples of generalized categories: metric spaces are a kind of enriched category and topological spaces are generalized multicategories for the ultrafilter monad.
But please do not let this bleed into a criticism of category theory as used in mathematics. Category theory from the very beginning was developed to help manage the complexity of modern mathematical fields like algebraic topology. It was then famously used by Grothendieck in algebraic geometry where some of the basic notions (schemes) were defined in terms of category theoretic concepts (functors). It's been applied to many other fields, since, including yes computer science, and mainly for the same purpose: giving precise terminology to common patterns (monads functors etc) and giving us the right concepts to design new functional programming languages. As someone who is an expert on these topics I find some of the popular sentiments about programmers using category theory to be a bit silly, but I'll admit it's overall probably good for my field because it cultivates a lot of interest in students. It probably plays a similar role to pop science/math in other fields: not very deep but fun and can be a gateway to "the real thing".
The popular perception of category theory is a bit bizarre to me though. It is a beautiful theory with many useful results. But you don't see the same excitement or resentment towards fields like order theory or abstract algebra, which are very closely related to, and just as abstract as, category theory and are used in similar ways.
The big thing IMO that makes Rust feel like Haskell is the pervasive use of traits and `#[derive(...)]` which is directly analogous to the pervasive use of typeclasses and `deriving` in Haskell.
Category theory isn't really a replacement for set theory any more than order theory is a replacement for set theory. What is important is not what your "foundational system" is, but that just like there are many concepts we learn in the context of set theory but are just very generally useful (equivalence classes, cardinality, injective/surjective functions), there are also similarly very useful concepts in category theory like adjoint functors, limits and universal mapping properties.
Basically,
1. You have a 0 time delta, and you can add and subtract them satisfying some natural equations. (time deltas form a group)
2. You can add time deltas to a datetime to get a new datetime, and this satisfies some natural equations relating to adding time deltas to each other (time deltas act on datetimes).
3. You can subtract two datetimes to get a time delta satisfying some more natural equations (the action is free and transitive).
In a cartesian closed category, if there is a function p : A -> (A -> B) that has a left-inverse, i.e., e : (A -> B) -> A with p o e = id_(A -> B) then B has a fixed point combinator Y : (B -> B) -> B, i.e., every function from B to itself has a fixed point: Y(f) = f(Y(f)).
The proof is like the Y combinator in untyped lambda calculus, but with extra ps and es. This is because one way to understand untyped lambda calculus is that you are working with a single type D that satisfies D = (D -> D) (so p,e are identities).
I like this because it makes the connection between the Y combinator and diagonalization arguments like Cantor's theorem explicit.
For instance, Cantor's theorem says that the powerset of a set always has higher cardinality. We can reformulate this as saying that there is no onto function p : X -> (X -> 2) because a subset of X is the same as a function from X to booleans (2 = {true, false}). An onto function has a left inverse (using axiom of choice) and so if we have an onto function X -> (X -> 2) then every function (2 -> 2) has a fixed point, but this isn't true! If we took Y(not) we would construct a boolean b : 2 such that b = not(b), which is impossible so we have a contradiction. I found this helpful in understanding why the "not" appears in just the right place in the classical proof.
WARNING: the below contains math. Ignore if math makes you mad.
If "side effects" means the availability of certain operations such as mutating state, throwing errors etc, then monads certainly do have something to do with side effects in that these operations can often be described by an algebraic theory and algebraic theories have a direct correspondence to certain kinds of monads (the monad of free algebras of the theory).
It's funny to see "low calorie" as a positive for an ideal food. From the perspective of getting people enough food to live, things like grains, corn/maize and potatoes are "ideal" foods because they can cheaply get us a significant portion of our needed calories.