[IlGrigiore]

This book does not talk about static typing, but about dependent types. Dependent types are more powerful and expressive than simple types because they convey more information. For example you could have [Int] to represent a list of numbers, but you could also have [x: Int, x > 20 && x < 50]. Or you could have an ordered array and know this fact by the type associated to the array. Moreover, you need to use a theorem prover to show that applying a function to a particular dependent type will result in the output dependent type. This kind of programming is not well suited to be implemented into typescript.

[k__]

So dependent types aren't static?

How does Idris solve this problem when compiling to JavaScript?

[nardi]

Dependent types are static. GP was trying to say that this book is about more than just normal static typing (of the kind that TypeScript adds to JavaScript).

There is no problem compiling dependent (or static) types to JaveScript, as the type checks are done at compile time, and don’t require any support from the JavaScript runtime.

[Naomarik]

That sounds like clojure spec.

[IlGrigiore]

Clojure spec is contract programming. You write pre and post conditions to ensure at runtime that Pre -> Program -> Post and every time you call a function pre and post conditions need to be checked. Dependent types analyze that relationship at compile time by proving that given the preconditions the function will produce the desired output. Since this is a compile time check you will not have a runtime penalty.