4 ms·

Fascinating! Now I'm curious, what causes this? Where does Turing completeness come from? Polymorphism? Inference? Higher-kinded types? (Probably not that last

• 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.
• AprilArcus 3y ago
  All you need is a way to branch and a way to loop, so anything with conditional types and recursive types will be Turing Complete