3 ms·

The title here is a truncated version of the original question because HN only allows 80-char titles. The question clarifies what I mean.

kybernetikos 13y ago
The question seems to indicate that you think of Haskells type system as sufficiently expressive (as opposed to some dependently typed language like agda or coq). There's lots of possible semantic information that might be useful to maintenance developers that would be a massive pain to encode into Haskells type system. More generally though, all of this seems to ignore what it might take to get the type system to do something for you. Just because you can make the type system check some property doesn't mean that it's a good use of your time. I can indicate to other developers a bunch of useful information by simply prefixing with c for Celsius if that's the convention for the codebase, but actually encoding all the rules that go along with that into the type system (e.g. no values allowed below -273.15) might not be a good use of my time. I think in the final analysis, the answer is no, because I could have a Hungarian prefix that meant 'is a string encoding a turing machine that halts when run on itself', but that's not something you're going to want your type system to try to check for you. Hungarian notation is all about encoding arbitrary semantic intention about variables into their name. Type systems can also encode arbitrary semantic intention (if they're expressive enough), but the effort associated with using them like that is much higher, just as the benefit is greater (since they're automatically checked). Therefore, while there is overlap, from an engineering point of view they don't cover exactly the same ground.
- rcthompson 13y ago
  I don't necessarily think of Haskell's type system as sufficiently expressive, it's just the most expressive type system that I'm familiar with, and it's also the type system in which I've seen cool examples implemented, such as the "catch SQL injections at compile time" example. I think you make some excellent points, and perspectives like this are exactly what I was looking for when I originally asked the question. So, I accepted an answer that says "yes", but "yes" won by default because every answer was either "yes", "no because HN is not even good enough to be a workaround", or irrelevant.

kybernetikos 13y ago

The question seems to indicate that you think of Haskells type system as sufficiently expressive (as opposed to some dependently typed language like agda or coq). There's lots of possible semantic information that might be useful to maintenance developers that would be a massive pain to encode into Haskells type system. More generally though, all of this seems to ignore what it might take to get the type system to do something for you. Just because you can make the type system check some property doesn't mean that it's a good use of your time. I can indicate to other developers a bunch of useful information by simply prefixing with c for Celsius if that's the convention for the codebase, but actually encoding all the rules that go along with that into the type system (e.g. no values allowed below -273.15) might not be a good use of my time. I think in the final analysis, the answer is no, because I could have a Hungarian prefix that meant 'is a string encoding a turing machine that halts when run on itself', but that's not something you're going to want your type system to try to check for you. Hungarian notation is all about encoding arbitrary semantic intention about variables into their name. Type systems can also encode arbitrary semantic intention (if they're expressive enough), but the effort associated with using them like that is much higher, just as the benefit is greater (since they're automatically checked). Therefore, while there is overlap, from an engineering point of view they don't cover exactly the same ground.

rcthompson 13y ago
I don't necessarily think of Haskell's type system as sufficiently expressive, it's just the most expressive type system that I'm familiar with, and it's also the type system in which I've seen cool examples implemented, such as the "catch SQL injections at compile time" example. I think you make some excellent points, and perspectives like this are exactly what I was looking for when I originally asked the question. So, I accepted an answer that says "yes", but "yes" won by default because every answer was either "yes", "no because HN is not even good enough to be a workaround", or irrelevant.