On Jun 22, 2007, at 2:46 PM, David Roundy wrote:
I think of top-level type declarations as type-checked comments, rather than a seat-belt. It forces you to communicate to others what a function does, if that function may be used elsewhere. I like this. Although it can be cumbersome for quick and dirty code, developers trying to read your code will thank you for it (unless you make *everything* top-level, which is just poor coding style).
-Wall -Werror isn't a seat belt, it's a coding-style guideline.
I don't think one can make blanket statements as to what type systems "are for". I doubt that the people who've dedicated their lives to type theory are doing so to provide style guidelines. I like the quick and open-ended definition that types are compile- time proxies for run-time values. It happens that current type systems are closely tied to propositional logic, because so many logicians are drawn to the work. This need not be the case. From this point of view, one pays attention to type theory because one produces the best code by providing the best guidance to the compiler. -Wall -Werror is establishing a contract to do so.