PinkLetter - Why retrofitting static types to JavaScript is hard

Welcome to my PinkLetter. A short, weekly, technology-agnostic, and pink newsletter where we cultivate timeless skills in web development.

My Ramblings This Week

This week, I sent Alexis King the following message:

One question I'm pondering is why implementation derives from types naturally but the other direction (i.e., typing an implementation) is hard and produces worse types (like in those JS packages to which TS types were added as an afterthought).

She was kind enough to blow my mind:

I think you actually have it somewhat backwards: abstractly, an implementation can always—in theory—give rise to types, but not the other way around, because types effectively describe an approximation of what the implementation does. This is easy to demonstrate, as there are many different functions of type String -> String, but given an implementation of a stringReverse function, it has exactly one type.

However, I suspect this isn’t really what you’re talking about. Rather, you’re wondering why it seems to be so much easier to use static typing when an implementation is designed with static types in mind, rather than trying to retrofit types onto an API designed using dynamic typing. The answer to that question comes from the way static type systems work. Every static type system is a collection of rules that classify programs into two categories: well-typed programs and ill-typed programs. Usually, we design type systems so that all well-typed programs are somehow “good”—that is, “well-typed programs don’t go wrong”—and we call such a type system “sound”. But this is hard, because it is provably impossible to write a decidable algorithm that identifies all good programs but no bad ones, given a Turing-complete programming language (this is Rice’s theorem).

So type systems have to make compromises. Instead of accepting all good programs, type systems accept that they will reject some good programs in addition to rejecting all the bad ones. The remaining set of good programs that they accept are the well-typed ones. But the choice of precisely which programs to accept and which ones to reject is a decision that has to be made for each type system, and different type systems can make radically different tradeoffs. For example, the Haskell type system is very structured, and it demands a very particular style of program construction, but in return it allows the programmer to express fairly complex things and still get decent type inference. The TypeScript type system, on the other hand, was explicitly designed to accommodate an existing style of programming, namely JavaScript programming, so it includes lots of rules to explicitly recognize JS idioms, which allows it to accept more good programs as well-typed.

A particularly good example of this is TypeScript’s support for narrowing based on control flow (https://www.typescriptlang.org/docs/handbook/2/narrowing.html). Most languages that were designed with static types from the start don’t support anything like this, because it requires fairly complex analysis of the code, and it’s easier to just add a different way of accomplishing the same thing. But TS supports this because it’s an idiom that JS programmers use all the time, so it has special logic in its typechecker to detect code patterned like this and use that to improve type inference.

In other words, TS actually goes to a fairly extensive effort to figure out what random JS programs are really doing and assign them some type. But in general, this is really hard, because again, a type system is just a particular set of rules made by the type system’s designer to try to capture some useful subset of “good programs”, and no matter how many rules you add, there will always, at least in theory, be some “good programs” that are not identified as well-typed. So gradual type systems like TypeScript will always be best-effort systems that try to identify as many good programs as possible within practical constraints.

However, when programs are written with static types in mind, this isn’t a problem, because the programmer knows how the static type system works. That allows the programmer to choose APIs and patterns that they already know the type system is good at identifying, i.e. they adopt a style that tends to “make the typechecker happy”. And it just so happens that the subset of “good programs” that the typechecker accepts is more than inclusive enough to have at least some way to express anything the programmer could possibly want to express, so the set of good programs that are rejected just aren’t considered. But this is really just the effect of the programmer adapting to take better advantage of the typechecker and writing programs that keep the typechecker in mind, not anything particularly deep or fundamental about programming or static typing.

One final point worth emphasizing is that this process by which the programmer adapts to the typechecker is specific to a given type system. The style of program construction that works well in TypeScript does not necessary carry over to other statically typed languages, since other languages have type systems that make totally different tradeoffs. So while the same basic principles do apply, the precise details of how things are encoded into the type system in Haskell are pretty different from how they’re encoded in TypeScript, and it’s important to keep in mind that each type system is just one point in an infinitely-large design space of static type systems. And due to the fundamental tradeoffs one has to make when designing a type system (by choosing which set of good programs you’re willing to reject), there can never be any “most powerful” type system—different type systems will always make different tradeoffs.

Elsewhere on the Web

Developer relations: (more than) the art of talking good by Emily Freeman

In my opinion, someone in developer relations serves as an advocate for the tech community within their company. And we do a lot more than go to conferences.

Riccardo: Great read on why devrel is about generativity (enabling the community).

Cloud SQLite by Brandur

This is one of those moments where we might legitimately be looking at a turning point for web technology – like when the combination of MySQL and PHP made it possible for anyone to build a dynamic, stateful application, or when Amazon changed the world with S3 and EC2. We could look back on this moment in ten years and think of monolithic programs like Postgres akin to how we think about Oracle today – hopelessly outdated in our modern world of fully distributed, streaming databases.

Riccardo: Good to see more NoSQL SQL stuff.

Why you should lift component state up to the URL by Sam Selikoff

"How can I sync component state with the URL?" This is one of the most common questions I see asked in the React community, and in this video we're going to learn why trying to synchronize state between your React app and the URL is a bad idea – and the right way to address this issue.

Riccardo: Shocking how simpler the code becomes when you pick the right abstraction.