Hacker News Reader

Comment by weeksie | Hacker News Reader

I explained that he _did_ test the program because he was writing a type. The type system by definition checks types.

I 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.

> 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

(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).

Some 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 :).

Some people argue that totality isn't enough, you really want a feasible (polytime) language.

http://www.di.unito.it/˜gaboardi/papers/BaillotGaboardiMogbi...

;-)

I 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.

Reply on news.ycombinator.com