4 ms·
> This matters because understanding that a normal type system is not Turing-complete means that there are truths it can't express. I thought Godel's incomplet
by cakoose 4y ago
> This matters because understanding that a normal type system is not Turing-complete means that there are truths it can't express.
I thought Godel's incompleteness theorem makes this true for all systems of proofs beyond a certain complexity. Does it matter whether the type system is Turing-complete or not?
(I don't have a robust understanding of Godel's incompleteness theorem.)
- nighthawk454 4y agoSure, but it is possible to be Turing-complete. There may be further things a Turing machine can never do, but we want to do at least that much. If the type system is not “fully powerful” in this way it may be lacking in some useful aspect.
- cakoose 4y agoYeah, but the phrasing seems likely to mislead. It sort of implies that a Turing-complete type system can express all truths.
- im3w1l 4y agoThe incompleteness theorem says there are some truths that can't be proven, but it doesn't say they can't be expressed.
- cakoose 4y agoWhen you run a type checker, it's proving that a program conforms to the type, right? That's why it seems like the incompleteness theorem applies. (Though as I mentioned before, I'm playing a bit loose with the logic.)