3 ms·
> not even accurate. What is not accurate in that post?
by sold 14y ago
> not even accurate.
What is not accurate in that post?
- weeksie 14y agoI explained that in the second paragraph.
- flatline3 14y agoThe author didn't claim that the system is alone sufficient "for any real world Haskell program", so your refutation appears rather spurious.
- weeksie 14y agoI explained that he _did_ test the program because he was writing a type. The type system by definition checks types.
- sold 14y agoI see what you mean, but it's rather bizzare to classify type checking as a form of testing, even if type system is very strong. Types and tests are different ways of specifying behaviour: tests are existential guarantees (output of the code sometimes has some properties), types are universal guarantees (output of the code always has some properties). In an ideal world, tests would be subsumed by types, but in reality tests can cover things that types do not.
- chimeracoder 14y ago> In an ideal world, tests would be subsumed by types It would be literally impossible for this to happen in a Turing-complete language, though, because a hypothetical 'perfect' type system would be able to solve the halting problem. The Haskell 'Bottom' type alludes to this in its documentation, actually: http://www.haskell.org/haskellwiki/Bottom http://www.haskell.org/haskellwiki/Bottom (Essentially, Bottom is a member of every type, or else the compiler would need to distinguish between a halting program and a non-halting program before accepting the input program).
- tikhonj 14y agoSome people argue that in an ideal world we wouldn't be using Turing-complete languages. Nothing like a total functional programming language to make life better :).
- GregBuchholz 14y agoSome people argue that totality isn't enough, you really want a feasible (polytime) language. http://www.di.unito.it/˜gaboardi/papers/BaillotGaboardiMogbil10esop-draft.pdf http://www.di.unito.it/˜gaboardi/papers/BaillotGaboardiMogbi... ;-)
- sold 14y agoI thought about total functional programming, like Agda. But even if you have Turing completeness, you can add time constraints to tests and everything will be decidable.