Minimalist And Maximalist Type Systems

post by adamShimi · 2024-07-05T16:25:59.448Z · LW · GW · 6 comments

This is a link post for https://epistemologicalfascinations.substack.com/p/minimalist-and-maximalist-type-systems

Contents

6 comments

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.

1. ^{^}

   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.

6 comments

Comments sorted by top scores.