I have two completely opposed aesthetic preferences inside me.
On one hand, I love minimalism: doing the maximum with as little as possible. This leads to a fascination with disciplines that have the smallest palette and the largest focus (calligraphy, go, writing, japanese cooking…). More abstractly, it’s an aesthetic of focus, of doing a single thing at a time. When in its thrall, I read a single book at a time for example, and ideally a book that requires deep understanding and analysis.
On the other hand, I love maximalism: doing everything at once in an explosion of parallels and alternatives and colors and sensations. Things like playing complex video games, or watching animation, or eating my family’s Tunisian recipes (abusively spicy!) And at the abstract level, it’s an aesthetic of exploration, of jumping from idea to idea, brainstorming and mixing and matching whatever comes to mind without polishing it too much.
I alternate between these two, often oscillating in the same day, sometimes spending weeks in only one mode.
And lately, I’ve noted this manifesting at the level of type systems.
We’ve been over this in the last couple of posts, but the gist is that a type system tries to capture what kind of operations can be done on the value used in a computer program, and to flag incompatible uses of such values before even running the program.
It’s a powerful tool, applied in many settings, and implemented in most programming languages. But like any core idea, you can run with it in wildly different ways.
The ML family of programming languages embodies the standard (academic) approach to type systems: types as mathematical constructs, and their combinations as logical combinations, following the Curry-Howard isomorphism. So using such a system let’s you breathe in the minimalism, the ascetism: you have a handful of basic types, a couple of operators, and you combine them cleanly and transparently and compositionally, such that it’s simple to build complex and yet sensible results from these building blocks.
It’s made so that you can think about it in your head without making massive mistakes, and you can know and even prove straightforwardly what will emerge from your manipulations. But that also makes it often more arid that it needs to be, forcing you to formalize in fundamental maths most of what you want to express. And it means too that you don’t get the really powerful features (like dependent types) unless they are thoroughly checked and rechecked and fit with everything else.
Then you have TypeScript. Whenever I use TypeScript, the main vibe is “What do you mean I can do that?”. It offers you insanely complex and powerful capabilities, to the point where you can almost write arbitrary type-level programs, including things as insane as string templating at the type-level! And all these features actually capture things practical programmers want to express, which means that you can very often find the right tool for your use case, even if that tool is actually part of a super complex and unusable fragment of dependent types or other advanced undecidable logical system.
But as a result, TypeScript also creates a lot more “Why can’t I do that?” moments. Because the rules for when you can’t combine things together, or you can combine them together and it breaks inference, or you can combine them together and it infers but it hides an error under the hood, are not clean, easy to compress boundaries. They emerge from the interaction of all the implementation of these ad-hoc features, which means that for predicting the behavior of some complex type, you need to know far more of the underlying gory details.
I’m french, which means that I was raised and trained heavily in the minimalist tradition. So I’m supposed to be disgusted by this kind of stuff, by this blatant blaspheme against sacro-saint soundness (ensuring you don’t let incorrect programs through)[1].
Yet I still find a sort of fascinating and horrifying beauty to TypeScript’s Type System. It has the feel of a crazily detailed and complex and often contradictory world that you have to explore and piece out for yourself, grabbing to passing comments on long lost PR for dear life — the From Software world of type systems.
If anything, TypeScript is even more fascinating because it shouldn’t work at all. It’s basically not made with all the structure that normally lets type systems stand strong, and yet it mostly does what you want. Yes there are bugs, and yes it will refuse apparently arbitrary combinations of features, but still… it does so much without completely exploding.
That being said, I expect that whenever I go back to a minimalist mood, I’ll start being frustrated again with this lack of focus and purity. Such is life.
- ^
TypeScript is unsound by design because it aims to provide gradual typing (adding types little by little) to untyped JavaScript. But even if that wasn’t the case, I expect its maximalist nature forces it to give up soundness — when you keep adding combinations of ad-hoc features, there’s no way you’re not introducing a ton of soundness bugs.
And there I thought with minimalist you meant Lisp and with maximalist Haskell or Lean.
It is definitely one minimalist vs maximalist dimensions ^^.
Thanks for these last three posts!
Just sharing some vibe I’ve got from your.. framing!
Minimalism ~ path ~ inside-focused ~ the signal/reward
Maximalism ~ destination ~ outside-focused ~ the world
These two opposing aesthetics is a well-known confusing bit within agent foundation style research. The classical way to model an agent is to think as it is maximizing outside world variables. Conversely, we can think about minimization ~ inside-focused (reward hacking type error) as a drug addict accomplishing “nothing”
Feels there is also something to say with dopamine vs serotonine/homeostasis, even with deontology vs consequentialism, and I guess these two clumsy clusters mirrors each other in some way (feels isomorph by reverse signe function). Will rethink about it for now.
As an aside note: I’m French too, and was surprised I’m supposed to yuck maximalist aesthetic, but indeed it’s consistent with my reaction reading you about TypeScript, also with my K-type brain.. Anecdotally, not with my love for spicy/rich foods ^^′
I see what you’re pointing out, but in my head, the minimalism and maximalism that I’ve discussed both allow you quick feedback loops, which is generally the way to go for complex stuff. The tradeoff lies more in some fuzzy notion of usability:
With the minimalism approach, you can more easily iterate in your head, but you need to do more work to lift the basic concepts to the potentially more tricky abstactions you’re trying to express
With the maximalist approach, you get affordances that are eminently practical, so that many of your needs are solved almost instantly; but you need to spend much more expertise and mental effort to simulate what’s going to happen in your head during edge-cases.
I’m obviously memeing a bit, but the real pattern I’m point out is more for “french engineering school education”, which you also have, rather than mere frenchness.
Interestingly, the Lean theorem prover is sometimes considered a bit of a mess type-theoretically. (an illustrative thread), but is perhaps the most popular theorem prover among mathematicians. I would say it’s more on the “maximalist” side.
Last I read about Rust’s type system, it basically didn’t have a theoretical basis, and seemed like it was just based around Graydon figuring out algorithms for getting the properties he wanted. Rust is much more popular than SML (or Haskell, though I’m not sure Haskell should really count as a ‘minimalist’ type system with all of its language extensions).
Didn’t know this about Lean, but the fact that a maximalist option is most popular with mathematicians makes sense to me. As someone who worked both with mathematicians and formal methods researchers (much more meta-mathematicians), the latter are much closer to programmers, in the sense that they want to build things and solve their own abstract problems, instead of necessarily wanting the most compositional machinery possible (although I still expect compositionality to be baked into the intuitions of many mathematicians).
Rust is an interesting point in the design space. If I had to describe it quickly according to the framing above, it feels like a really pleasant fractal tradeoff between different type systems:
It has basically affine type but with more practical usage through borrowing (see this survey for more details)
It has an ML type system with algebraic datatypes (and even traits which are close to typeclasses in Haskell)
So it definitely feels more maximalist than some ML or some pure linear type system, but that’s more from the combination and UX work than from a crazy “let’s add this super advanced feature” rush à la TypeScript imo.