28 ms·
A turing complete system doesn't necessarily mean it's powerful, or useful, it just means that it's equivalent with a turing machine and in the case of type sys
by bad_user 9y ago
A turing complete system doesn't necessarily mean it's powerful, or useful, it just means that it's equivalent with a turing machine and in the case of type systems, that usually happens because general recursivity is allowed.
And that can also mean that it is error prone.
- fauigerzigerk 9y agoIt doesn't mean useful, but in my opinion it definitely means powerful. Being expressive enough to describe any possible algorithm is a power. No self respecting super hero would deny that, not even TypeScript's worst enemy. But with every power comes a weakness. Compile times can no longer just seem endless. They can actually be endless, and there is no way to prove otherwise. What I find unconvincing about many Turing complete type systems is that pragmatically speaking they are really shitty general purpose programming languages. If we create Turing complete type systems and suffer the consequences, why not go all the way and make it actually practical to write proper meta programs the way Lisp has done?
- bad_user 9y agoI kind of disagree, describing any possible algorithm is not that powerful, given that an actual Turing machine can do it. And along with Turing machines you've got problems, like undecidability and the halting problem.