Type Safety Doesn't Matter (2023)

The title is pure click bait, the title suggest that type safety doesn't matter, but then the author explains why it does matter e.g. catching errors at compile time instead of run time. A better title would be "My take on type safety".

So this basically summarizes as &quot;A) the goal is to reduce runtime errors so manage your time well, also B) linting tools are good at doing that quickly&quot;?<p>I feel like it could really use a couple examples of situations where type safety is a waste of time. As-is the post vaguely suggests a tradeoff and doesn&#x27;t elaborate.

It doesn&#x27;t just move errors to compile time. It moves runtime errors into the interface layer where you parse a request to bind it into your type so that by the time it reaches the persistence layer or something deeper you don&#x27;t need to bubble up validation errors. You measure your invariants at the boundaries to provide safety to your interior code (defensive programming) and provide meaningful errors messages to users (developer experience).

&gt; This may sound pedantic and click-baity<p>exactly, it&#x27;s clickbait

In a 100m sprint, running fast does not matter, it&#x27;s crossing the line very early that is.

I agree completely with the premise and the conclusion, however I would not describe types as moving errors to compilation time, but as moving effort to the earliest parts of the workflow: more time spent on writing code, more time spent on thinking before doing, more time spent on specifying your interfaces. Agreed on the diminishing return as well: use them as long as your leverage (= time saved debugging &#x2F; (writing time + reviewing time + maintenance time)) is good, maintenance time in particular is often overlooked: how much time will it take to train the new recruit so that the understand your oh-so-smart custom types?

Clickbait, and they didn&#x27;t even provide any examples to illustrate their point.

He wrote: &quot;What I mean is that, on its own, type safety is not important. It’s only useful because of what it accomplishes&quot;.<p>It&#x27;s like saying: &quot;This food, on its own, is not important. It&#x27;s only useful because it provides me energy&quot;.

[deleted]

&gt; This may sound pedantic and click-baity, but in my opinion it’s a vitally important distinction with real world ramifications.<p>Add <i>per se</i> at the end of the title and it’s not clickbait any more.<p>Language is a thing.

For those dinging the article, please check this line<p>&gt; when discussing architecture of code or reviewing a pull request, I will often times push back on changes that add more complexity in the type system. The reason is because, even if a change adds “type safety,” this extra complexity is only warranted if it achieves our primary goal, namely reducing runtime errors.<p>It&#x27;s poorly emphasized, but the author is referring to Typescript-style static typing which can come with a truck load of complexity. Something like Go&#x27;s type system is fine (there&#x27;s nothing sophisticated about it) but Typescript&#x27;s type system gives you enough rope to hang yourself with.

&gt; It’s only useful because of what it accomplishes: moving errors from runtime to compile time.<p>...<p>&gt; Bug reduction is not the only benefit of strong typing. There’s also: easier codebase maintainability, simplicity of refactoring, new engineering onboarding, potentially performance gains, and probably a few other things I missed.<p>But besides that, what have the Romans ever done for us?

It is a very simple blog post, it makes a simple point, but I also think it is a very important point: Types are a means to an end.<p>I am implementing Practal in TypeScript, and it is so much more productive than if I had to do it in JavaScript. I am (mostly) not using any advanced features of the type system, but use it for its simple features, as described in this blog post. The greatest feature: I can ignore the type system, where it makes sense. That isn&#x27;t as bad as it might sound, given that the type system of TypeScript is not sound in the first place.<p>The blog post suggests also thinking about other means to achieve the end (less bugs), such as push-button technology like static analysis. I agree with this, but am more interested in another direction of developing this thought: If we are actually proving theorems in a logic about mathematical objects like code, we don&#x27;t need a type system, either. In fact, a type system can and will get in the way of formulating your theories in the simplest and most elegant way. It adds the additional constraint that on top of figuring out how to express something mathematically, you also need to figure out how to express it <i>in this particular type system</i>. And while often these two things are aligned well enough, this is not always the case. By the way, note that I am not saying that <i>types</i> themselves are not always useful. They are. It is just that we don&#x27;t need a static type system to use types, which I think of as abstract sets.<p>Let me anticipate a comment someone will make: But type systems are how in practice logic is implemented, what are you talking about?! And yes, if you look at the main systems in the space, like Isabelle, Lean, Coq, they are based on type systems. But that is not how it necessarily needs to be done. You could be using first-order logic, like Mizar does, but that comes with its own set of restrictions, mainly missing out on higher-order features. What I am implementing in Practal instead is <i>Abstraction Logic</i> [1], which is higher-order, but based on a single mathematical universe instead of types.<p>Now, right now that is a far cry from the push-button alternatives the blog post suggests, but a) it is not opposed to these alternatives, but an additional angle to view things from, and b) it is becoming much more push-button than it used to be with the help of increasing compute power and AI.<p>[1] <a href="http:&#x2F;&#x2F;abstractionlogic.com" rel="nofollow">http:&#x2F;&#x2F;abstractionlogic.com</a>