<p>Some languages have type systems complex enough to embed undecidable problems in the type system. <a href="https://sdleffler.github.io/RustTypeSystemTuringComplete/" rel="noreferrer">This famous post</a> details implementing a Turing-complete language in Rust's type system, and Swift's type checker has been proven undecidable in multiple distinct ways: <a href="https://forums.swift.org/t/swift-type-checking-is-undecidable/39024" rel="noreferrer">1</a> <a href="https://forums.swift.org/t/termination-checking-for-type-substitution/64504" rel="noreferrer">2</a> <a href="https://forums.swift.org/t/two-more-undecidable-problems-in-the-swift-type-system/64814" rel="noreferrer">3</a>. C++'s template system has also been proven Turing-complete <a href="https://stackoverflow.com/a/275295/6253337">on StackOverflow</a>, and there's <a href="https://github.com/microsoft/TypeScript/issues/14833" rel="noreferrer">an open issue on TypeScript</a> about its system being Turing-complete.</p>
<p>These languages all have very useful features in their type systems, but that ultimately led to their own undecidability. In at least some cases, these issues weren't known when the relevant features were first proposed, e.g. in Swift:</p>
<blockquote>
<p>We are also aware of examples where we don't manage to canonicalize types properly, causing miscompiles and crashes. We've been fixing these gradually over time, but we continue to discover more problems as we fix them. This was a strong hint that the underlying approach was not correct, which is why I spent some time thinking about the fundamentals of this problem. Indeed, we can now see that the reason we have struggled with correctness in this area of the language is that a solution is <em>impossible</em> in the general case.</p>
</blockquote>
<p>Is it possible to rigorously prove type checking to be decidable? What work must be done when extending a type system to avoid the compiler becoming impossible to implement?</p>

<language-design><type-checker><computability>
How to prevent undecidable type systems?
CC BY-SA 4.0
2023-07-05T20:18:16.423Z
Do note that even Java's type system, which is pretty limited, is Turing-complete. You might need to heavily restrict it to make sure it's not Turing-complete (or add a termination checker that you can opt out of?).
user
CC BY-SA 4.0
2023-07-05T20:20:11.693Z
@user Interesting, do you have a source for that? Part of me wonders if this is one of the differences between Java and C#, but either way it's good to know that you don't need a powerful type system to run into this.
Bbrk24
CC BY-SA 4.0
2023-07-05T20:21:49.047Z
Here's the paper proving it: [Java Generics are Turing Complete](https://arxiv.org/abs/1605.05274).
user
CC BY-SA 4.0
2023-07-05T22:31:52.557Z
"Drop turing completeness and embrace totality" is one option - see for example [idris](https://docs.idris-lang.org/en/latest/tutorial/theorems.html#sect-totality) or lean. I'll leave a proper answer to the mathematicians.
Bruce Adams
CC BY-SA 4.0
2023-07-05T23:09:05.803Z
@user interestingly, Kotlin's are not
Seggan
CC BY-SA 4.0
2023-07-05T23:20:55.240Z
@BruceAdams I'd be interested to see a full answer from that.
Bbrk24
CC BY-SA 4.0
2023-07-06T12:06:52.673Z
c# is also Turing complete
Oscar Smith
CC BY-SA 4.0
2023-07-06T17:15:52.517Z
@Bbrk24 Bruce Adams' suggestion means turning your type system into something like Lean or Agda, with a termination checker like I suggested, requiring laborious proofs for everything. I'm not sure that's what you want
user
CC BY-SA 4.0
2023-07-06T17:21:36.610Z
@user And I’m not familiar enough to say. Hence why I would be interested in an answer detailing how that works, or explaining the costs and benefits of such an approach.
Bbrk24
<blockquote>
<p>Is it possible to rigorously prove type checking to be decidable?</p>
</blockquote>
<p>Well that's the whole problem, there isn't an effectively computable function for doing so ;)</p>
<blockquote>
<p>What work must be done when extending a type system to avoid the compiler becoming impossible to implement?</p>
</blockquote>
<p>You need some kind of formal model, so that when you implement a type checker for your new feature, you can attempt to prove that it is correct.</p>
<p>The specific Swift issue you quoted was resolved a while ago. The compiler now deals with recursive associated types by pre-computing an internal representation on which all queries are resolved in finitely many steps; the pre-computation rejects the problematic cases: <a href="https://forums.swift.org/t/the-requirement-machine-a-new-generics-implementation-based-on-term-rewriting/55601" rel="noreferrer">https://forums.swift.org/t/the-requirement-machine-a-new-generics-implementation-based-on-term-rewriting/55601</a></p>

CC BY-SA 4.0
2023-08-10T15:41:34.553Z
2023-08-10T15:41:34.553Z
Slava Pestov
CC BY-SA 4.0
2023-11-07T13:08:25.623Z
Someone re-proved its TCness [by implementing BrainFuck](https://forums.swift.org/t/brainf-in-the-swift-type-system/68301), though it has a truly horrid memory footprint.
Bbrk24
CC BY-SA 4.0
2023-08-10T15:50:49.243Z
Oh hey, funny seeing you here. Welcome to the site! It makes sense that the first issue has since been resolved, but what about the most recent one? That one was only posted in May of this year.
Bbrk24
<blockquote>
<p>Is it possible to rigorously prove type checking to be decidable?</p>
</blockquote>
<p>Yes. Doing this is generally quite similar to proving any recursive algorithm decidable: you make inductive arguments about the structure of the algorithm. Type <em>checking</em> is known to decidable for most theoretical type systems considered useful, but most real languages also involve some amount of type <em>inference</em>, which can become undecidable much more easily. Still, many type inference algorithms have been proven decidable as well; the <a href="https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system" rel="noreferrer">Hindley–Milner algorithm</a> is one of the most well-known.</p>
<p>However, decidability proofs are far rarer for the type systems used in real languages. One reason for this is that it requires formally specifying the type system, which almost no languages do. Most languages are either informally specified using English prose (such as C, C++, and Java) or not specified at all. Another reason is that decidability is just generally not enormously <em>useful</em>: in practice, the type system can be artificially made decidable by adding arbitrary recursion limits to heuristically detect infinite loops.</p>
<p>The essential question to ask is: what does decidability of a typechecking algorithm afford you? On its own, the answer is “very little”. Even a decidable algorithm can be made to take arbitrarily long to complete, so it doesn’t guarantee your typechecker will terminate in your lifetime. In contrast, type system features that introduce undecidability (which are often some form of generic programming) can be enormously practically useful.</p>
<blockquote>
<p>What work must be done when extending a type system to avoid the compiler becoming impossible to implement?</p>
</blockquote>
<p>As implied above, decidability is not by any means necessary to make a typechecker possible to implement, it just means it might not terminate on some programs. And as mentioned above, this issue can usually be practically avoided by simply adding recursion depth limits.</p>
<p>That is not to say there aren’t real difficulties in implementing efficient checking and inference algorithms for complex type systems that behave usefully on real programs. Type system design is a broad and complex subject. But decidability is not usually one of the major implementation obstacles.</p>

CC BY-SA 4.0
2023-07-05T21:37:45.077Z
2023-07-05T21:37:45.077Z
Alexis King
# How to prevent undecidable type systems?
Posted by: username_0 on 2023-07-05
Some languages have type systems complex enough to embed undecidable problems in the type system. [This famous post](https://sdleffler.github.io/RustTypeSystemTuringComplete/) details implementing a Turing-complete language in Rust's type system, and Swift's type checker has been proven undecidable in multiple distinct ways: [1](https://forums.swift.org/t/swift-type-checking-is-undecidable/39024) [2](https://forums.swift.org/t/termination-checking-for-type-substitution/64504) [3](https://forums.swift.org/t/two-more-undecidable-problems-in-the-swift-type-system/64814). C++'s template system has also been proven Turing-complete [on StackOverflow](https://stackoverflow.com/a/275295/6253337), and there's [an open issue on TypeScript](https://github.com/microsoft/TypeScript/issues/14833) about its system being Turing-complete.

These languages all have very useful features in their type systems, but that ultimately led to their own undecidability. In at least some cases, these issues weren't known when the relevant features were first proposed, e.g. in Swift:

> We are also aware of examples where we don't manage to canonicalize types properly, causing miscompiles and crashes. We've been fixing these gradually over time, but we continue to discover more problems as we fix them. This was a strong hint that the underlying approach was not correct, which is why I spent some time thinking about the fundamentals of this problem. Indeed, we can now see that the reason we have struggled with correctness in this area of the language is that a solution is *impossible* in the general case.

Is it possible to rigorously prove type checking to be decidable? What work must be done when extending a type system to avoid the compiler becoming impossible to implement?
**Tags:** language-design type-checker computability
> **Comments:**
> **username_1**: Do note that even Java's type system, which is pretty limited, is Turing-complete. You might need to heavily restrict it to make sure it's not Turing-complete (or add a termination checker that you can opt out of?).  
> **username_0**: @user Interesting, do you have a source for that? Part of me wonders if this is one of the differences between Java and C#, but either way it's good to know that you don't need a powerful type system to run into this.  
> **username_1**: Here's the paper proving it: [Java Generics are Turing Complete](https://arxiv.org/abs/1605.05274).  
> **username_2**: "Drop turing completeness and embrace totality" is one option - see for example [idris](https://docs.idris-lang.org/en/latest/tutorial/theorems.html#sect-totality) or lean. I'll leave a proper answer to the mathematicians.  
> **username_3**: @user interestingly, Kotlin's are not  
> **username_0**: @BruceAdams I'd be interested to see a full answer from that.  
> **username_4**: c# is also Turing complete  
> **username_1**: @Bbrk24 Bruce Adams' suggestion means turning your type system into something like Lean or Agda, with a termination checker like I suggested, requiring laborious proofs for everything. I'm not sure that's what you want  
> **username_0**: @user And I’m not familiar enough to say. Hence why I would be interested in an answer detailing how that works, or explaining the costs and benefits of such an approach.  
---
## 2 answers
### Answer by username_6 on 2023-07-05. Score: 25
> Is it possible to rigorously prove type checking to be decidable?

Yes. Doing this is generally quite similar to proving any recursive algorithm decidable: you make inductive arguments about the structure of the algorithm. Type *checking* is known to decidable for most theoretical type systems considered useful, but most real languages also involve some amount of type *inference*, which can become undecidable much more easily. Still, many type inference algorithms have been proven decidable as well; the [Hindley–Milner algorithm](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system) is one of the most well-known.

However, decidability proofs are far rarer for the type systems used in real languages. One reason for this is that it requires formally specifying the type system, which almost no languages do. Most languages are either informally specified using English prose (such as C, C++, and Java) or not specified at all. Another reason is that decidability is just generally not enormously *useful*: in practice, the type system can be artificially made decidable by adding arbitrary recursion limits to heuristically detect infinite loops.

The essential question to ask is: what does decidability of a typechecking algorithm afford you? On its own, the answer is “very little”. Even a decidable algorithm can be made to take arbitrarily long to complete, so it doesn’t guarantee your typechecker will terminate in your lifetime. In contrast, type system features that introduce undecidability (which are often some form of generic programming) can be enormously practically useful.

> What work must be done when extending a type system to avoid the compiler becoming impossible to implement?

As implied above, decidability is not by any means necessary to make a typechecker possible to implement, it just means it might not terminate on some programs. And as mentioned above, this issue can usually be practically avoided by simply adding recursion depth limits.

That is not to say there aren’t real difficulties in implementing efficient checking and inference algorithms for complex type systems that behave usefully on real programs. Type system design is a broad and complex subject. But decidability is not usually one of the major implementation obstacles.
---
### Answer by username_5 on 2023-08-10. Score: 6
> Is it possible to rigorously prove type checking to be decidable?

Well that's the whole problem, there isn't an effectively computable function for doing so ;)

> What work must be done when extending a type system to avoid the compiler becoming impossible to implement?

You need some kind of formal model, so that when you implement a type checker for your new feature, you can attempt to prove that it is correct.

The specific Swift issue you quoted was resolved a while ago. The compiler now deals with recursive associated types by pre-computing an internal representation on which all queries are resolved in finitely many steps; the pre-computation rejects the problematic cases: <https://forums.swift.org/t/the-requirement-machine-a-new-generics-implementation-based-on-term-rewriting/55601>
> **Comments:**
> **username_0** (2023-08-10): Oh hey, funny seeing you here. Welcome to the site! It makes sense that the first issue has since been resolved, but what about the most recent one? That one was only posted in May of this year.  
> **username_0** (2023-11-07): Someone re-proved its TCness [by implementing BrainFuck](https://forums.swift.org/t/brainf-in-the-swift-type-system/68301), though it has a truly horrid memory footprint.  
---
