The Seven Sources of Unsoundness in TypeScript

[danvk]

The Seven Sources of Unsoundness in TypeScript

https://effectivetypescript.com/2021/05/06/unsoundness/

[danvk]

Comment by Tamás Hegedűs on 2022-01-25 12:51:

Great article! I would disagree with this statement:

How often does this occur? Surprisingly rarely

If you came with a static typed language background, then I would say it occurs rather often :)

[danvk]

Comment by danvdk on 2022-02-06 03:43:

Thanks! My point is just that, putting my paranoid hat on, I'd expect to run into inaccurate types from third-party libraries all the time. The surprise is because, while this does happen from time to time, it's certainly not a constant problem, at least not for me.

If you're frequently running into inaccurate third-party types, I'm curious which library is the issue.

[KATT]

Great read! 🙏

[tylim88]

assigning any type or asserting type is not the reason for unsoundness because you deliberately make it unsafe

an example would be dart language, you can also assert type and assign any(dynamic) type which makes it unsafe, but dart is still considered as a sound language

soundness is more like how predictable the type is

[danvk]

@tylim88 Thanks for pointing me at Dart, I hadn't read about it in quite a while. The Dart language guide provides a definition for unsoundness:

What is soundness?
Soundness is about ensuring your program can’t get into certain invalid states. A sound type system means you can never get into a state where an expression evaluates to a value that doesn’t match the expression’s static type.

So sound = every expression's static type matches its runtime type. This is the definition that this post uses.

It looks like Dart achieves soundness by inserting runtime checks, which is outside the scope of static analysis and not something that TypeScript would do. From skimming the docs, it also looks like it suffers from unsoundness if you ever use a JS library (Source 4: Inaccurate type definitions).

Dart is an interesting example of a language making different choices than TS and landing on a different place in the ease of use ↔ soundness spectrum.

[3Shain]

Great article.

There are five turtles

I think this can't demonstrate unsoundness but incompleteness. According to the definition:

• sound: all incorrect programs are rejected
• complete: all correct programs are accepted

And the 'turtle cutoff' may reject correct program, which could give soundness but definitely shows incompleteness.

EDIT: maybe the 'turtle cutoff' can accept incorrect program but this need to be proved. I'm confident about incompleteness (and I'm sure this is what the video talk about - there is a limit on recursive type checking ,so that you can construct a correct but rejected program) but not sure about unsoundness (to which the existence of limit is still not sufficient).

By the way there is a new example

function iife(fn: ()=>void) {
    fn();
}

iife(()=>{
    console.log(`variable is ${variable}`);
})
let variable = 0;

This can be type checked but throws Uncaught ReferenceError: variable is not defined at runtime. The callback is deliberately executed right away, and it will work if replacing iife with setTimeout. However, the type system can't tell you whether the callback is invoked immediately.