Re:Ask HN: A well-typed program won't go wrong?
by dragonwriter on Monday November 03, 2014 @05:22PM
(#8553945)
I think at least 3, and maybe all four, are true from various perspectives:
1. I think that the scenario here is one that Haskell can type check, though it takes some work. But I'm not sure.
2. Haskell's type system is better than many, but limited. Coq/Agda/Idris are more powerful.
3. One common definition of "going wrong" is "returning an incorrect answer". Crashing isn't going wrong in that framework. (I don't necessarily agree with it, though I've seen it; at any rate, there is a good reason to think that crashing is a lesser problem than executing and returning incorrect results.)
4. While there may be definitions of "well-typed programs" and "go wrong" for which this is true, ISTR that they are either ones which make it so that a type system that completely supports general computation is not possible, or ones ones which require excluding a lot of errors from "going wrong".
1. I think that the scenario here is one that Haskell can type check, though it takes some work. But I'm not sure.
2. Haskell's type system is better than many, but limited. Coq/Agda/Idris are more powerful.
3. One common definition of "going wrong" is "returning an incorrect answer". Crashing isn't going wrong in that framework. (I don't necessarily agree with it, though I've seen it; at any rate, there is a good reason to think that crashing is a lesser problem than executing and returning incorrect results.)
4. While there may be definitions of "well-typed programs" and "go wrong" for which this is true, ISTR that they are either ones which make it so that a type system that completely supports general computation is not possible, or ones ones which require excluding a lot of errors from "going wrong".