Comment by fsloth | Hacker News Reader

Comment by fsloth | Hacker News Reader

This topic of "what are static types good for" continued to bug me because I could not formulate a concrete answer to myself. I found the following Reddit discussion

http://www.reddit.com/r/programming/comments/lirke/simple_ma...

Which had eventually the specific thing I was after in a comment by Rich Hickey which helped to nail the concept I was after

"Statically typed programs and programmers can certainly be as correct about the outside world as any other program/programmers can, but the type system is irrelevant in that regard. The connection between the outside world and the premises will always be outside the scope of any type system."

Which is precisely why I enjoy types: Self referential consistency makes sure I do not make errors within the logical model I have set for myself. It does not help me build better models but once those models are built it helps me to compose programs that do not break the invariants in the chosen formalism.

Which, I think tells exactly what static types are good for: For those sort of problems that benefit from having a formal specification. There are a lot of programs that have this quality.

So the argumentation is a bit skewed off. It should not be about whether static or dynamic types are better but more focus on what are those identifiable problem patterns where a dynamic type system helps programmer create more value than a static one and vice versa.

> Self referential consistency makes sure I do not make errors within the logical model I have set for myself. It does not help me build better models but once those models are built it helps me to compose programs that do not break the invariants in the chosen formalism.

I think this is a valid point.

But I am less convinced about the second part. I feel that better type systems do help one model the world better (while retaining the consistency checking that you mentioned). In my mind at least having more/better "type tools" is like having differently shaped pieces in your lego tool box. You can create better models for yourself, because the pieces allow you to. And the more experience you have with them, your modeling abilities also improve.

The thing about "the outside world" is that it is just one form of interpretation of a chunk of code. Inarguably, it is the most important one, but once you recognize that it is not alone in that regard you get a very new appreciation for "internal consistency".

Ultimately, this becomes an issue of "minimize your interfaces" which is widely known to be close to vital for writing successful code. If you can "purify" most of your code base then use types to ensure that it has internal consistency then the remaining task is to write (at least) one valid, trusty "interpreter" from your pure/trusted codebase into the real world.

This is undoubtedly the most fragile piece of your application!

But it's also eminently library-able and it places the risk-burden over a tiny fraction of your code. It's also the place where you want to property/unit/integration test the hell out of the world.

So all of the standard CS adages apply again, but thanks to purity/type-checking you've reduced the risk exposure to a tiny fraction of what it is while using other tools.

Reply on news.ycombinator.com