3 ms·
It's simple. A type system can be complicated to itself do computations. See dependent types, for instance. Once you open that up you have the full range of com
by jerf 5y ago
It's simple. A type system can be complicated to itself do computations. See dependent types, for instance. Once you open that up you have the full range of complications for computing itself in your type system. There are type systems sufficiently complicated to declare "the type of Turing Machines that halt in a finite amount of time" as a type; this causes obvious problems.
It is a well-known phenomenon that it can take surprisingly little to turn a computation system Turing complete; witness, for instance, C++'s accidentally-Turing-complete templates. So it can wiggle in without you even realizing it at design time. Or, if you're using a type system with sufficient power like dependent types, it is surprisingly easy to put together four or five recursive types that, on their own, are all perfectly computable, but together turn out to create something that is Turing complete. Write a program with a few hundred of these and Turing completeness is almost bound to sneak in somewhere.
See https://www.gwern.net/Turing-complete https://www.gwern.net/Turing-complete , and ponder applications to just-slightly-too-powerful type theories. Or https://github.com/Microsoft/TypeScript/issues/14833 https://github.com/Microsoft/TypeScript/issues/14833 .