Hacker News Reader

Comment by sandGorgon | Hacker News Reader

I know that typescript doesn't have advanced types, but can a book like this be adapted to use typescript ?

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.

So dependent types aren't static?

How does Idris solve this problem when compiling to JavaScript?

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.

That sounds like clojure spec.

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.

Typescript actually does have some forms of type dependency (eg. conditional types), but these things have been added in a sort of ad-hoc way, and it's unclear how sound they actually are, and they are quite limited. The book here uses a language, pie, that is designed in a much more principled way, with greater expressiveness. The book probably won't be directly applicable to TS work, but I'm sure you would benefit from getting a more rounded understanding of what is possible with type systems.

Reply on news.ycombinator.com