3 ms·
> 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 hypo
by 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.