On: Rust's type system is Turing-complete (2017)

[TheCoelacanth]

It's easy enough to turn a non-terminating type checker into a terminating one, just add a recursion limit.

[continuational → TheCoelacanth]

That makes it nearly impossible for the programmer to predict what will type check and what will not.

[dataflow → continuational]

So what? We can't predict how much RAM the user's machine has either, but that doesn't mean we can't write useful programs.

[viuphiet → continuational]

This isn't a problem at all for modern type systems. OCaml, Haskell, and even C++ have Turing complete type systems and this is one of the last concerns for developers.

[mannerheim → viuphiet]

I believe Haskell's type system is only Turing complete with UndecidableInstances or other extensions. But these extensions are not uncommon.

[TheCoelacanth → continuational]

Not really, I can predict that anything I will actually do that has valid types will type check.

Some pathological valid cases invented by someone trying to break the type checker, might not type check.

[knome → continuational]

for c++, I know both clang and gcc make the template resolution depth accessible to the developer via a compiler flag, allowing those that bypass the reasonable defaults to extend that depth.