3 ms·
Turing completeness doesn't have to come from a single feature, it often comes from a combination of features. e.g. the interaction between subtyping (e.g. inh
by ynik 3y ago
Turing completeness doesn't have to come from a single feature, it often comes from a combination of features.
e.g. the interaction between subtyping (e.g. inheritance) and generics (with variance) is tricky: https://www.cis.upenn.edu/~bcpierce/papers/variance.pdf https://www.cis.upenn.edu/~bcpierce/papers/variance.pdf
It can be highly nontrivial to tell if a language actually has a Turing complete type system: the 2007 Kennedy&Pierce paper made it likely that java was turing complete; but it took until 2016 until it was finally proven that to be turing complete (https://arxiv.org/abs/1605.05274 https://arxiv.org/abs/1605.05274).
> What would it take a for a type system to NOT become Turing complete?
An analysis of all possible interactions between all features in the type system, building a formal proof that the type system is not turing complete. This is not really realistic for the style of complex generic type systems that programmers are now used to, it would need to be a vastly simpler language.