3 ms·

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 discu

by fsloth 12y ago

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_made_easy_by_rich_hickey_video/ 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.

shadowfox 12y ago
> 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.
- fsloth 12y ago
  The Lego analogy is what I also often like to use :) ! " I feel that better type systems do help one model the world better" I agree. But then again, I prefer to start from scribbling mathematical proof mimicking pseudocode which is easily transferred then to statical types. Some people just bang something together, prototype on the IDE/REPL as they go on and they can probably finish faster than me and produce value. If this figure-this-out-while-coding person then has the craftmanship to clean up the code the result is often as good as with the paper-and-pen-first approach. For larger systems, however, I would claim that starting from careful design pays off more because the code-prototype can quickly get out of hands if there are too many abstractions and variables flying in the air at the same time. The 'formal' approach has pitfalls if applied without taste or experience, since, well, modeling for modelings sake can get out of hands at which point one has a shaking tower of abstraction generated from mental masturbation rather than anything of lasting value. This becomes pathological the minute it reaches production. I think we recognize it all has to do with the experience of the programmer and the dedication but craftmanship is very hard to formalize...
tel 12y ago
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.

by fsloth 12y ago

shadowfox 12y ago

> 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.

fsloth 12y ago
The Lego analogy is what I also often like to use :) ! " I feel that better type systems do help one model the world better" I agree. But then again, I prefer to start from scribbling mathematical proof mimicking pseudocode which is easily transferred then to statical types. Some people just bang something together, prototype on the IDE/REPL as they go on and they can probably finish faster than me and produce value. If this figure-this-out-while-coding person then has the craftmanship to clean up the code the result is often as good as with the paper-and-pen-first approach. For larger systems, however, I would claim that starting from careful design pays off more because the code-prototype can quickly get out of hands if there are too many abstractions and variables flying in the air at the same time. The 'formal' approach has pitfalls if applied without taste or experience, since, well, modeling for modelings sake can get out of hands at which point one has a shaking tower of abstraction generated from mental masturbation rather than anything of lasting value. This becomes pathological the minute it reaches production. I think we recognize it all has to do with the experience of the programmer and the dedication but craftmanship is very hard to formalize...

tel 12y ago

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.