[whilenot-dev]

Sure, but the author picked TypeScript nonetheless. TypeScript is not a runtime, but a mere type checker - JavaScript is the runtime and a highly dynamic language. This detail got somehow completely lost in the article, but is IMHO the main culprit why such validations aren't bad, or sometimes even preferred.

The article also skipped over the following related topics:

  - When would you wrap errors from lower levels as your own?
  - What does "parse don't validate" mean when a TypeScript library gets transpiled to JavaScript?

[chongli]

You don’t need a runtime for dependent types. After type checking the types get erased during compilation.

[whilenot-dev]

Nobody would question that, but publishing a JavaScript library means that anyone using plain JavaScript can make use of it. Even though you aren't ever in control of the toolchain of your library's users, it's still your responsibility - as library author - to take that differences into account. If you'd transpile your library from Idris to JavaScript and publish it, these validations just can't be neglected at runtime. Type systems are just another model of the world at runtime.