On Wed, Jun 25, 2014 at 11:47:23AM -0400, Michael Orlitzky wrote:
On 06/25/2014 11:24 AM, Francesco Ariis wrote:
For non-believers, here is a blog post that opened my eyes on the matter [1].
None of that helps if you write the wrong program. Your program may typecheck, but if you're expecting "42" as output and your program hums the Star Trek theme instead, the fact that it correctly does the wrong thing won't be much consolation.
data Hum = HumStarTrekTheme | CountrySong data UltimateAnswerToEverything = FourtyTwo {- assorted datatypes and functions -} program :: a -> UltimateAnswerToEverything Getting serious again, the author of the post states: " A type system can be regarded as calculating a kind of static approximation to the run-time behaviours of the terms in a program. and then delivers (i.e. |order zero (suc b) = ge ge0| won't typecheck). I cannot but feel 90%+ of tests are just an "ad hoc, bug ridden, informally specified" type system.