From 09b5ab14d8440d661de3255080d64384e9d39145 Mon Sep 17 00:00:00 2001 From: josh11b Date: Mon, 13 Nov 2023 16:15:25 -0800 Subject: [PATCH] Link to Swift undecidable type-system problems (#3394) --- docs/design/generics/details.md | 14 ++++++++------ docs/design/generics/goals.md | 15 +++++++++------ 2 files changed, 17 insertions(+), 12 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index dc16eb9648f6..5a629b64be26 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -4634,12 +4634,14 @@ This problem can also result from a chain of `impl` declarations, as in `A impls B` if `A* impls C`, if `Optional(A) impls B`, and so on. Determining whether a particular set of `impl` declarations terminates is -[equivalent to the halting problem](https://sdleffler.github.io/RustTypeSystemTuringComplete/) -(content warning: contains many instances of an obscene word as part of a -programming language name), and so is undecidable in general. Carbon adopts an -approximation that guarantees termination, but may mistakenly report an error -when the query would terminate if left to run long enough. The hope is that this -criteria is accurate on code that occurs in practice. +equivalent to the halting problem (content warning: contains many instances of +an obscene word as part of a programming language name +[1](https://sdleffler.github.io/RustTypeSystemTuringComplete/), +[2](https://forums.swift.org/t/two-more-undecidable-problems-in-the-swift-type-system/64814)), +and so is undecidable in general. Carbon adopts an approximation that guarantees +termination, but may mistakenly report an error when the query would terminate +if left to run long enough. The hope is that this criteria is accurate on code +that occurs in practice. Rule: the types in the `impl` query must never get strictly more complicated when considering the same `impl` declaration again. The way we measure the diff --git a/docs/design/generics/goals.md b/docs/design/generics/goals.md index 7fb7858bca8d..93ca3f42602b 100644 --- a/docs/design/generics/goals.md +++ b/docs/design/generics/goals.md @@ -316,12 +316,15 @@ Some of this is likely unavoidable or too costly to avoid, as most existing checked generics systems [have undecidable aspects to their type system](https://3fx.ch/typing-is-hard.html), including [Rust](https://sdleffler.github.io/RustTypeSystemTuringComplete/) and -[Swift](https://forums.swift.org/t/swift-type-checking-is-undecidable/39024). We -fully expect there to be metaprogramming facilities in Carbon that will be able -to execute arbitrary Turing machines, with infinite loops and undecidable -stopping criteria. We don't see this as a problem though, just like we don't -worry about trying to make the compiler reliably prevent you from writing -programs that don't terminate. +Swift ([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), +[4](https://forums.swift.org/t/brainf-in-the-swift-type-system/68301)). We fully +expect there to be metaprogramming facilities in Carbon that will be able to +execute arbitrary Turing machines, with infinite loops and undecidable stopping +criteria. We don't see this as a problem though, just like we don't worry about +trying to make the compiler reliably prevent you from writing programs that +don't terminate. We _would_ like to distinguish "the executed steps are present in the program's source" from "the compiler has to search for a proof that the code is legal." In