Comment by z3t4

TypeScript is sadly very unsound by design, so doing this kind of thing in TypeScript is always going to be more “best effort” and less “exhaustive proof.” That’s not necessarily wrong or bad per se, as after all, Haskell has escape hatches, too (and so do dependently-typed languages, for that matter). However, there are philosophical differences between the way the languages’ type systems are designed.

When I’ve talked to people who develop and use TypeScript, the general impression I’ve gotten from them is that TS is actually as much about tooling as it is about correctness. TS enables things like autocomplete, jump to definition, and quick access to documentation, and it does that by leveraging the typing information to “see through” the dynamic dispatch that makes that sort of thing infeasible in dynamically-typed JavaScript. The TS type system does provide some correctness benefits, don’t get me wrong, but where ease of use and correctness are in conflict, usually ease of use is preferred.

This is true even with all the “strictness” options enabled, like strict null checking. For some examples of TypeScript unsoundness, see [1] and [2]. Flow is actually generally a lot better than TS in this regard (though it does still have some major soundness holes), but it looks like TS has basically “won,” for better or for worse. But again: TS won because its tooling was better, not because its ability to actually typecheck JS programs was better, which I think reinforces what I said in the previous paragraph on what TS is really about.

[1] https://twitter.com/lexi_lambda/status/1068704405124452352

[2] https://twitter.com/lexi_lambda/status/1068705142109810688

This SO answer is pretty clever: https://stackoverflow.com/a/56006703

type NonEmptyArray<T> = [T, ...T[]];

That is: A type of "NonEmptyArray" of T is an array of one element of type T, followed by any number of type-T elements.

I recently [0] updated my Control Flow Graph representation in a Typescript parser for AVM1 bytecode because I had the exact same issue as in the article. I previously represented my graph as an array of blocks. But a graph always has at least one block (the entry point). The old representation forced me to check for the empty case despite knowing that valid graphs always have at least one block.

Here is the old representation:

    export interface Cfg {
      blocks: CfgBlock[];
    }

And here is the new one:

    export interface Cfg {
      head: CfgBlock;
      tail: CfgBlock[];
    }

Switching to this new representation allowed to then simplify code manipulating this graph. This representation is also simple enough that most schema validators can represent it.

You still have to note that with this representation you no longer have a single array. It's not an issue in my case but your situation may vary. You may try the tuple-based solution mentioned in a sibling comment if you need to have a single array.

[0] https://github.com/open-flash/avm1-types/commit/ec85efab8c9e...