22 ms·
> simple type checking becomes undecidable Where can I read more about this?
by porridgeraisin 2y ago
> simple type checking becomes undecidable
Where can I read more about this?
- btilly 2y agoIt follows from Turing completeness. See https://en.wikipedia.org/wiki/Turing_completeness https://en.wikipedia.org/wiki/Turing_completeness. It takes very little for a system to become Turing complete. And once it is, you can include arbitrary computations. Proving that they stop is impossible in general due to the well-known Halting problem. https://beza1e1.tuxen.de/articles/accidentally_turing_complete.html https://beza1e1.tuxen.de/articles/accidentally_turing_comple... offers examples showing how easy it is to accidentally get Turing completeness, including multiple widely used type systems.
- deleted 2y ago[deleted]
- bubblyworld 2y agoTypescript's type system is technically undecidable because you can interpret Turing machines with it: https://github.com/microsoft/TypeScript/issues/14833 https://github.com/microsoft/TypeScript/issues/14833 The flip side is that such systems can still be practically useful. You just have to manage your type complexity, much like you already manage your runtime complexity.
- ted_dunning 2y agoThis book does it well. It can be a heavy slog: https://mitpress.mit.edu/9780262536431/the-little-typer/ https://mitpress.mit.edu/9780262536431/the-little-typer/ Here is a free book on how type checking can be used to do mathematical proofs: https://lean-lang.org/functional_programming_in_lean/ https://lean-lang.org/functional_programming_in_lean/