Basically, Evan decided he wanted Elm to be a pre-packaged closed ecosystem where it was easy to develop very simple standalone apps, but made it very difficult to impossible to actually integrate with any existing JavaScript code or libraries. This was a baffling decision to people who thought Elm was supposed to be a practical language.
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.
You can do something like this with OCaml/SML's module system.
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.
Typed functional languages like Haskell (data)/ML (type) do have a built-in way to define new tree types, and so does Rust (enum). It's one of the biggest things I miss when I'm not using these languages, especially when combined with some metaprogramming (deriving/derive) to get some functions defined for these new types very quickly.
I'll be surprised if none of the bigger beer companies ends up buying it for the brand and history alone. But maybe it doesn't have as much name recognition as I thought.
It really is remarkable. I think the most remarkable fact about it is that the intensional identity type was invented by Martin Lof in the 70s, the groupoid model was discovered in the 90s and then finally in the late 2000s various people made the connection that Martin Lof's original system from the 70s was in a sense already a type theory for abstract homotopy theory. This led to an explosion of new ideas in type theory (univalence, higher inductive types, modalities) that took a somewhat obscure field of math/cs to the thriving research community it is today.
> How can roots be changed without a redo of the universe?
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.
WASM is not really an assembly language. Before this, WASM didn't have jump at all, and so tail calls are adding a form of jump (jump with arguments). This makes WASM a much better compilation target.
Basic results that are useful on a day-to-day basis:
1. Yoneda's Lemma, and the corollary that objects defined by universal property are unique up to unique isomorphism
2. Right adjoints preserve limits and more generally, Kan extensions
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.
It sounds like category theory likely has no direct impact on your life. So you can move on.
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.
It doesn't have to be one or the other :). OCaml and Haskell are two great languages that the Rust designers were familiar with.
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.