4 ms·
It's easy enough to turn a non-terminating type checker into a terminating one, just add a recursion limit.
by TheCoelacanth 6y ago
It's easy enough to turn a non-terminating type checker into a terminating one, just add a recursion limit.
- continuational 6y agoThat makes it nearly impossible for the programmer to predict what will type check and what will not.
- viuphiet 6y agoThis 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 6y agoI believe Haskell's type system is only Turing complete with UndecidableInstances or other extensions. But these extensions are not uncommon.
- knome 6y agofor 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.
- dataflow 6y agoSo 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.
- TheCoelacanth 6y agoNot 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.