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 think we might be speaking past each other? How is enum in Rust a tree type? You might be able to use it to create a tree type, but that's no different from using struct to make struct Tree : std::vector<Tree> {}; in C++. That wouldn't mean C++ has a tree type, it just means it's not hard to create your own. Whereas std::list is actually a linked list type that's already there.
Well, std::list is something you can create with C++ code (and likely is in most implementations of C++?), it doesn't need any special support. So I can see why someone might not treat std::list as any more special than a tree datastructure supplied by a different library?
However, algebraic data types really make your life easier, and more languages should have them.
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.
Anchor Steam had its place, 20+ years ago. It had a long-standing tradition of being a beer that stood the test of time, head and shoulders above the usuals of the time.
The problem is they failed to continue to keep up with the times as the proliferation of truly fantastic beers hit and later dominated the scene. Take a look through their flagships; they look more like what any new and likely-soon-to-close brewery will start with (a hazy, a west coast, a porter, a lager, and an ale) rather than a brewery steeped in 100+ years of history and brewing mastery.
Anchor Steam may have had the brand recognition necessary to survive in an overcrowded market say 10 years ago, but now people are flocking to the breweries themselves and are not as tied down into a single brand as they used to be.
It's sad but in the same way that any long-standing brand that couldn't keep up with the Joneses and went out of business is sad. Not really in any other way.
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.
I’ll admit to coming late to the party (when a friend introduced me in 2013), but what’s amazing to me is when you take the step of encoding your cellular structures as adjacency matrices.
You can visually see structures of your theory (eg, facts about groups) in the patterns of terms in the matrix.
Eg, diagramming a cyclic group ends up with a banding pattern in the portion of your matrix denoting equivalent pairs under the operation… which shows that in some sense, the level maps of + on Zn x Zn form a twisted torus. (Which makes sense in hindsight, as you have the product of two loops with the level maps wrapping around non-trivially.)
That you get ideas such as that by chasing through a purely abstract definition (groups -> diagrams) is wild to me.
Edit:
I actually built a simple case (Z4) in Minecraft — just because I found it surprising.
> 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.
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 sounds like category theory likely has no direct impact on your life. So you can move on.
Very dismissive statement that misses the person's point.
> It is a beautiful theory with many useful results.
But what are those results? Besides Yoneda, are there insightful, surprising, delightful results? I personally gave up on my CT study after seeing that it was just chapter after chapter of definitions and nothing else.
I always compare it to abstract algebra. AA can be studied without any connection whatsoever to the physical world or even to numbers -- as "abstract" as math can get. And yet from the first chapter you are hit with surprising theorems, and they continue non-stop, challenging your brain at every turn. I fail to see this in CT.
This is what turned me off also. Category theory is all promises of potential benefits, but none seem to have materialised.
The closest example to something useful I’ve seen is a CT-based explanation for why Automatic Differentiation is formulated the way it is.
However, AD was invented before CT, and the explanation didn’t add any value that I could see. It didn’t result in a “better” AD, it simply attached esoteric labels to existing things.
There are plenty of interesting results in category theory, in fact your comparison to abstract algebra is apt. There is only so much you can say about an arbitrary group in general, or an arbitrary topological space, just like there is only so much you can say about an arbitrary category.
> Very dismissive statement that misses the person's point.
I read it as acknowledging that you shouldn't feel like you have to spend time on things that provide you no value. That seems to directly acknowledge the point I took from the earlier comment, which is that they keep spending time on it and coming away with no idea what they even should be getting from it, much less getting anything specifically.
(I like category theory, but it's a reasonable reaction for most people. I'd love for more people to engage with it on its merits, but also, people have finite time and may rather spend it on things they derive joy from.)
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.
What is your recommendation for learning? I've been recommended Bartosz Milewski enough times, and started to dive in. I am not interested in learning the totality of Category theory, just enough to be more effective in FP languages like Haskell.
Category Theory will not make you more efficient in FP languages like Haskell. I studied it enough to realise that it doesn’t give me any insights or thinking tools I can actually use to write better software. However I highly recommend reading “Software Foundations”. It is almost guaranteed to make you better at writing software in any language. Including Haskell. That’s what happened to me.
Have you been recommended his blog series/book only, or the playlists on YouTube as well? I really like his recorded lectures on YouTube and they cover similar ground in a similar order to the blog posts (from what I've read—I'm further into the YouTube series than I am his written material).
You don't need to learn category theory to be more effective in FP languages like Haskell. Category theory was used as inspiration for design of ML and Haskell, but it is not necessary for programming in them.
Weirdly, I don’t love or hate category theory but I get very excited about order theory and abstract algebra in software. It feels lonely exploring them compared to other things, which is funny to say. It’s not fully explored or the new hotness.
It's because the lack of practical applications. People can make broken abstractions without knowledge of the fundamentals like compositions or functors and still get their shit to work.
That matters more to engineers then true understanding. So a lot of engineers end up trying to understand it and when they fail they easily move on to other things because it's not required knowledge for their job.
category theory has a very hard "k" sound at the front and a g sound which is also hard, which makes people react more strongly to the name than order theory or abstract algebra.
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.