Relatedly, I found this out the hard way yesterday evening: https://stackoverflow.com/questions/66631251/overflow-evalua...
Rust's type system is Turing-complete (2017)
21–30 of 91 posts
Re: Rust's type system is Turing-complete (2017)
#22Earlier quoted context omitted.
It’s a consequence of Goedels incompleteness theorem. You cannot create a type system that stops if the program is type valid, and does not stop (or stops indicating invalid) if the program is type invalid. The practical consequences of this are (probably) minimal.
The proof is trivial. The valid proofs in Zfc are ennumerable. Let f be a proposition in zfc that is undecidable in zfc. Write a computer program c that checks for a proposition p whether proof number n is a proof of p for all n. Apply that computer program to p. A rust program that is valid iff c(p) either doesn’t stop type checking or is invalid.
Do you mean apply program c to proposition f? That is compute c(f)? Of course no one disputes that if one encoded this in Rust's type system, Rust will enter an infinite loop. That's the point of this article.
But none of this has to do with whether Rust's type system is sound or complete as a type system, only that as a logic it is undecidable.
Re: Rust's type system is Turing-complete (2017)
#23It’s important to understand that this is a big problem. If a type system is Turing complete, than it either has to be inconsistent or incomplete. In other words it either must allow type invalid programs through, or it must prevent some type valid programs (or both!).
Out of curiosity — has there ever been a type system that was discovered to be Turing-complete and then actually have caused a bug for a real application that was caused by the fact that it allowed an invalid program through? I'm specifically not talking about something like Typescript which is widely known to be unsound, but a type system that was believed to be "safe" before someone figured it is Turing complete.
[deleted]
Re: Rust's type system is Turing-complete (2017)
#24One of the reasons I like weak type systems or duck typing as is with vanilla JS is because I don't have cognitive overload... I don't have to think about abstractions as types I only need to think how to solve the problem in front of me. My unit tests can check for correctness after I've solved the problem. The fact that you can have Turing completeness in a type-system (not the language itself but within it's type…
You do realize that you're moving part of the cognitive load until later and increasing it when you have to implement a type checker in unit tests for every program you write.
Yes and?
I have the full power of the language to force type correctness instead of some janky meta language.
Re: Rust's type system is Turing-complete (2017)
#25Earlier quoted context omitted.
The proof is trivial. The valid proofs in Zfc are ennumerable. Let f be a proposition in zfc that is undecidable in zfc. Write a computer program c that checks for a proposition p whether proof number n is a proof of p for all n. Apply that computer program to p. A rust program that is valid iff c(p) either doesn’t stop type checking or is invalid.
Do you mean apply program c to proposition f? That is compute c(f)? Of course no one disputes that if one encoded this in Rust's type system, Rust will enter an infinite loop. That's the point of this article. But none of this has to do with whether Rust's type system is sound or complete as a type system, only that as a logic it is undecidable.
Yes (changed the post)... my point is that the program is valid! Rusts type system can fail to stop on valid programs. I’m probably making a mess of all this though and should shut up before I confuse things more!
Re: Rust's type system is Turing-complete (2017)
#26To me the main takeaway of results like this is: you're already paying the full price of using whatever complicated type system feature you care to name. So I have limited sympathy for people who are scared of the complexity of, say, higher-kinded types, or dependent types, or kind polymorphism. Your type system is already as complicated as possible, adding more features won't make it more Turing-complete - rather, m…
I strongly disagree. Just because a feature doesn’t increase the underlying theoretical complexity doesn’t mean it’s a good idea. As a trivial example C plus “come from” is fundamentally the same language as regular C, and one can trivially translate it to remove come from. That doesn’t mean that adding come from to C would be a good idea.
For anyone confused like me. [1]
Incidentally, Googling "C plus come from" only returns two relevant results, the parent comment and a manual for an esoteric programming language called C-INTERCAL that uses the COME FROM statement and compiles to C. [2]
Re: Rust's type system is Turing-complete (2017)
#27It’s important to understand that this is a big problem. If a type system is Turing complete, than it either has to be inconsistent or incomplete. In other words it either must allow type invalid programs through, or it must prevent some type valid programs (or both!).
> In other words it either must allow type invalid programs through, or it must prevent some type valid programs (or both!). I don't see how this is the case. The type system being Turing complete just makes it undecidable, ie. it's not guaranteed to finish type checking. In a way you could call that "preventing some type valid program", though I wouldn't consider an infinite loop of types valid.
Which doesn't matter that much because there is a fairly small limit on how deep recursion can go which you can easily exceed without Turing-completeness, and the distinction between a program that will halt eventually but not within the limit you give it and one that will never halt doesn't matter for practical purposes.
Re: Rust's type system is Turing-complete (2017)
#28Earlier quoted context omitted.
Do you mean apply program c to proposition f? That is compute c(f)? Of course no one disputes that if one encoded this in Rust's type system, Rust will enter an infinite loop. That's the point of this article. But none of this has to do with whether Rust's type system is sound or complete as a type system, only that as a logic it is undecidable.
Yes (changed the post)... my point is that the program is valid! Rusts type system can fail to stop on valid programs. I’m probably making a mess of all this though and should shut up before I confuse things more!
Also I obviously fucked up the trivial proof. What I want to write is a rust program that type checks iff an an undecidable true proposition is true! But c doesn’t do that
Re: Rust's type system is Turing-complete (2017)
#29To me the main takeaway of results like this is: you're already paying the full price of using whatever complicated type system feature you care to name. So I have limited sympathy for people who are scared of the complexity of, say, higher-kinded types, or dependent types, or kind polymorphism. Your type system is already as complicated as possible, adding more features won't make it more Turing-complete - rather, m…
I disagree. A terminating type checker is much more valuable than a possibly non-terminating one. Also I think you're possibly conflating multiple issues here. Higher-kinded types, dependent types and kind polymorphism don't actually mean your type system becomes undecidable. They do vastly complicate the implementation in other ways, though.
It's easy enough to turn a non-terminating type checker into a terminating one, just add a recursion limit.
Re: Rust's type system is Turing-complete (2017)
#30One of the reasons I like weak type systems or duck typing as is with vanilla JS is because I don't have cognitive overload... I don't have to think about abstractions as types I only need to think how to solve the problem in front of me. My unit tests can check for correctness after I've solved the problem. The fact that you can have Turing completeness in a type-system (not the language itself but within it's type…
I have the inverse experience. I find it far more cognitively burdensome to have to keep track of the types without annotations or assistance from a type checker. Getting rid of the type checker doesn’t make the type go away, it just means the full burden of managing them correctly falls on the programs. And it’s not for lack of effort—I’ve been using Python among other languages for 15 years, but I would still find…
What kind of types are you dealing with that makes them so hard to keep track of? Are you talking about strings and integers, or a really really complicated objects and functions thing with functions of functions of functions and that kind of thing?