作者探讨了自身在审美偏好上的两种极端：极简主义与极繁主义，并将其映射到编程语言中的类型系统上，以 TypeScript 和 ML 语言为例，分别代表了极繁与极简两种风格。TypeScript 拥有强大的功能，但其复杂性也带来了一些挑战，而 ML 语言则以其简洁性和严谨性著称。作者认为，TypeScript 类型系统虽然看似混乱，却具有独特的魅力，其不拘一格的设计和强大的功能使其成为一个值得探索的领域。

🤔 作者将自身的审美偏好映射到编程语言的类型系统上，将 TypeScript 归类为极繁主义风格，而 ML 语言则代表极简主义风格。 TypeScript 拥有强大的功能，可以实现复杂的类型级编程，甚至包括字符串模板等功能。其强大的功能来源于对各种类型组合和操作的灵活支持，但这也导致了规则复杂、边界模糊等问题。 例如，TypeScript 允许在类型级进行字符串模板，这在 ML 语言中是不可想象的，但这也意味着 TypeScript 的类型系统更加复杂，需要开发者理解更多的细节才能预测其行为。 作者认为，TypeScript 类型系统就像一个错综复杂的迷宫，需要开发者不断探索和理解，才能掌握其精髓。

🤯 作者认为 TypeScript 类型系统虽然复杂，但其设计理念和功能实现方式却具有独特的魅力，即使其不符合传统的类型系统设计原则，它仍然能够有效地工作。 TypeScript 的设计目标是为 JavaScript 提供渐进式类型化，这意味着它需要兼容 JavaScript 的各种特性，这在一定程度上导致了其类型系统的不完整性和不一致性。 然而，作者认为 TypeScript 类型系统在功能强大和兼容性之间取得了平衡，其设计理念和实现方式值得借鉴和学习。

🧐 作者认为 TypeScript 类型系统虽然不符合传统的类型系统设计原则，但它仍然能够有效地工作。 TypeScript 类型系统的设计目标是为 JavaScript 提供渐进式类型化，这意味着它需要兼容 JavaScript 的各种特性，这在一定程度上导致了其类型系统的不完整性和不一致性。 然而，作者认为 TypeScript 类型系统在功能强大和兼容性之间取得了平衡，其设计理念和实现方式值得借鉴和学习。 作者还强调了 TypeScript 类型系统的不确定性，即其行为难以预测，这可能导致一些难以察觉的错误。 因此，作者建议开发者在使用 TypeScript 时要谨慎，并注意其类型系统的复杂性和不确定性。

🤩 作者认为 TypeScript 类型系统虽然不符合传统的类型系统设计原则，但它仍然能够有效地工作。 TypeScript 类型系统的设计目标是为 JavaScript 提供渐进式类型化，这意味着它需要兼容 JavaScript 的各种特性，这在一定程度上导致了其类型系统的不完整性和不一致性。 然而，作者认为 TypeScript 类型系统在功能强大和兼容性之间取得了平衡，其设计理念和实现方式值得借鉴和学习。 作者还强调了 TypeScript 类型系统的不确定性，即其行为难以预测，这可能导致一些难以察觉的错误。 因此，作者建议开发者在使用 TypeScript 时要谨慎，并注意其类型系统的复杂性和不确定性。 作者最后总结道，TypeScript 类型系统虽然不完美，但它仍然是一个值得探索的领域，其强大的功能和独特的设计理念值得开发者学习和借鉴。

🥺 作者认为 TypeScript 类型系统虽然不符合传统的类型系统设计原则，但它仍然能够有效地工作。 TypeScript 类型系统的设计目标是为 JavaScript 提供渐进式类型化，这意味着它需要兼容 JavaScript 的各种特性，这在一定程度上导致了其类型系统的不完整性和不一致性。 然而，作者认为 TypeScript 类型系统在功能强大和兼容性之间取得了平衡，其设计理念和实现方式值得借鉴和学习。 作者还强调了 TypeScript 类型系统的不确定性，即其行为难以预测，这可能导致一些难以察觉的错误。 因此，作者建议开发者在使用 TypeScript 时要谨慎，并注意其类型系统的复杂性和不确定性。 作者最后总结道，TypeScript 类型系统虽然不完美，但它仍然是一个值得探索的领域，其强大的功能和独特的设计理念值得开发者学习和借鉴。

Published on July 5, 2024 4:25 PM GMT

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.

Discuss