carbon-language/carbon-lang
1
0
Fork 0
mirror of https://github.com/carbon-language/carbon-lang.git synced 2026-09-24 19:20:13 +01:00
Code Issues Packages Projects Releases 10 Wiki Activity

Link to Swift undecidable type-system problems (#3394)

Browse Source
This commit is contained in:
josh11b
2023-11-14 00:15:25 +00:00
committed by GitHub
parent 2715e2276e
commit 09b5ab14d8
2 changed files with 17 additions and 12 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/design/generics/details.md
+8 -6
View File
@@ -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
docs/design/generics/goals.md
+9 -6
View File
@@ -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