[porridgeraisin]

> simple type checking becomes undecidable

Where can I read more about this?

[btilly]

It follows from Turing completeness. See 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_comple... offers examples showing how easy it is to accidentally get Turing completeness, including multiple widely used type systems.

[ted_dunning]

This book does it well. It can be a heavy slog:

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/

[bubblyworld]

Typescript's type system is technically undecidable because you can interpret Turing machines with it:

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.