Tradeoffs of Highly-Expressive Types

A better-argued, less ranty version of a blog post I wrote some time ago which generated some interesting discussions here, and to which the article above is a reply / complement.

I think the prime number example (if obviously artificial) illustrates well the point I also wanted to make: while it might be technically possible to perfectly represent this function's I/O with the type system, what are the benefits and what are the costs? We seem to broadly agree that, as one approaches type perfection, benefits get smaller while costs grow bigger. A classic engineering tradeoff.

I also really liked how the author highlights the differences between application code and library code, which I hadn't taken much into consideration in my post. For example, I really didn't think about how using a library can be frustrating in many other ways, not only types! But, as he notes, we're accustomed to that, so it goes more unnoticed. And I really like the idea of having features in the language that allow encapsulating types. No clue what they could look like (I don't have strong CS foundations, so I'm out of my depth here), but the idea sounds very appealing.