Hacker News Reader

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

View on HN

The incompleteness theorem says there are some truths that can't be proven, but it doesn't say they can't be expressed.

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

Sure, 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.

Yeah, but the phrasing seems likely to mislead. It sort of implies that a Turing-complete type system can express all truths.

Reply on news.ycombinator.com