# Two more undecidable problems in the Swift type system

**URL:** <https://forums.swift.org/t/two-more-undecidable-problems-in-the-swift-type-system/64814>\
**Category:** Compiler\
**Created:** [May 4, 2023, 2:59pm UTC](https://forums.swift.org/t/two-more-undecidable-problems-in-the-swift-type-system/64814 "2023-05-04T14:59:19Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![Slava\_Pestov](https://sea2.discourse-cdn.com/swift/user_avatar/forums.swift.org/slava_pestov/32/30204_2.png) [@Slava\_Pestov](https://forums.swift.org/u/Slava_Pestov)\
**Post date:** [May 4, 2023, 2:59pm UTC](https://forums.swift.org/t/two-more-undecidable-problems-in-the-swift-type-system/64814/1 "2023-05-04T14:59:19Z")

</div>

Previously:

- [Encoding the word problem for an arbitrary semi-group in a protocol where clause](https://forums.swift.org/t/swift-type-checking-is-undecidable/39024)
- [Encoding a tag system with type substitution](https://forums.swift.org/t/termination-checking-for-type-substitution/64504)

# Conditional conformances

The first construction uses [SE-0143](https://github.com/apple/swift-evolution/blob/main/proposals/0143-conditional-conformances.md). (Rust also has conditional conformances, and here is a writeup with a similar construction, except it uses an interpreter for the Smallf%#$\* programming language, in place of a tag system: [Rust's type system is Turing complete](https://sdleffler.github.io/RustTypeSystemTuringComplete/). Also, here is a bug report where a user inadvertedly wrote an infinite loop with conditional conformances in Swift: [[SR-6724] Swift 4.1 crash when using conditional conformance · Issue #49273 · swiftlang/swift · GitHub](https://github.com/apple/swift/issues/49273). I've been thinking about this problem for a while now.)

Consider an expression involving a qualified name lookup like `foo.bar`. If `foo` conditionally conforms to some protocol `Q`, and `Q` defines a method named `bar`, then the result of the name lookup depends on this conditional conformance. Is name lookup a decidable problem in the Swift type system?

You start with an encoding of a tag system from the type substitution example, but without the Next associated type. In the type substitution post, the Next associated type encoded the computation; but the below construction shows that you doesn't need that and it is possible to encode the computation in other ways.

```swift
protocol P {
  associatedtype A: P
  associatedtype B: P
  associatedtype C: P
  associatedtype T: P
}

struct Halt: P {
  typealias A = Halt
  typealias B = Halt
  typealias C = Halt
  typealias T = Halt
}

struct End: P {
  typealias A = AA<End>
  typealias B = BB<End>
  typealias C = CC<End>
  typealias T = Halt
}

struct AA<T: P>: P {
  typealias A = AA<T.A>
  typealias B = AA<T.B>
  typealias C = AA<T.C>
}

struct BB<T: P>: P {
  typealias A = BB<T.A>
  typealias B = BB<T.B>
  typealias C = BB<T.C>
}

struct CC<T: P>: P {
  typealias A = CC<T.A>
  typealias B = CC<T.B>
  typealias C = CC<T.C>
}

```

So far, everything is decidable. Here, the protocol P is pretty simple and the conformances all have very simple type substitution rules.

But then, you add another protocol Q and declare some conditional conformances to model the tag system evaluation:

```swift
protocol Q {}

extension Halt: Q {}
extension End: Q {}
extension AA: Q where T.T.B.C: Q {}
extension BB: Q where T.T.C: Q {}
extension CC: Q where T.T.A.A.A: Q {}

func foo<T: Q>(_: T.Type) {}

foo(AA<AA<AA<End>>>.self)

```

Now, to check that `AA<AA<AA<End>>>` conforms to `Q`, you have to evaluate the tag system:

```swift
aaa => abc => cbc => caaa => aaaaa => aaabc => abcbc
=> cbcbc => cbcaaa => caaaaaa => aaaaaaaa => aaaaaabc
=> aaaabcbc => aabcbcbc => bcbcbcbc => bcbcbca
=> bcbcaa => bcaaa => aaaa => aabc => bcbc => bca
=> aa => bc => a => halt

```

This reduces to `Halt: Q`, which conforms unconditionally.

Interestingly, if you actually try the above example, it fails with a circular reference. There might be a bug there because the Collatz sequence for n=3 does not actually have a non-trivial cycle (if it did for any n, that would disprove the conjecture!).

# SIL type lowering

As part of constructing SIL from the syntax tree, the compiler must determine calling conventions by flattening out value types into atomic leaves.

Consider these modified definitions of AA, BB and CC:

```swift
struct End: P {
  typealias A = AA<End>
  typealias B = BB<End>
  typealias C = CC<End>
  typealias T = Halt

  var t: Halt
}

struct AA<T: P>: P {
  typealias A = AA<T.A>
  typealias B = AA<T.B>
  typealias C = AA<T.C>

  var t: T.T.B.C
}

struct BB<T: P>: P {
  typealias A = BB<T.A>
  typealias B = BB<T.B>
  typealias C = BB<T.C>

  var t: T.T.A
}

struct CC<T: P>: P {
  typealias A = CC<T.A>
  typealias B = CC<T.B>
  typealias C = CC<T.C>

  var t: T.T.A.A.A
}

```

Now, to compute the lowering for a type like this, the compiler also has to evaluate the Collatz sequence for n=3, because you get a series of nested fields t, t.t, t.t.t, ... until eventually one of the t.t.t.t...t.t.t's is 'Halt', which is an empty struct.

```swift
struct S {
  var t: AA<AA<AA<End>>>
}

```

Now, the point is not that the termination of these algorithms hinges on the Collatz conjecture---any tag system can be encoded this way, and tag systems are Turing complete. A universal Turing machine would require a tag system built out of 578 concrete types, which would be unweildy, but they would be mechanically constructed in the same way as the AA/BB/CC types for the Collatz sequence.

It's interesting that all four examples I've constructed so far depend on [SE-0157](https://github.com/apple/swift-evolution/blob/main/proposals/0157-recursive-protocol-constraints.md), basically pushing the limits of the interactions between this feature and different parts of the compiler. I wonder if there are any hidden Turing machines that do not depend on this feature.

In the fullness of time, we could convert conditional conformance checking and SIL type lowering into iterative algorithms which could impose a maximum iteration count, and instaed of crashing and blowing the stack they could emit breadcrumb diagnostics showing the sequence of substitutions which took place.

---

<div class="post-metadata">

**Author:** ![bbrk24](https://sea2.discourse-cdn.com/swift/user_avatar/forums.swift.org/bbrk24/32/27370_2.png) [@bbrk24](https://forums.swift.org/u/bbrk24)\
**Post date:** [May 15, 2023, 11:38pm UTC](https://forums.swift.org/t/two-more-undecidable-problems-in-the-swift-type-system/64814/2 "2023-05-15T23:38:19Z")

</div>

> [@Slava\_Pestov](#):
>
> Interestingly, if you actually try the above example, it fails with a circular reference. There might be a bug there because the Collatz sequence for n=3 does not actually have a non-trivial cycle (if it did for any n, that would disprove the conjecture!).

I believe I have found an error in your encoding. According to Wikipedia, the rules are `a` -\> `bc`, `b` -\> `a`, and `c` -\> `aaa`. However, the extension you have written has `b` -\> `c`, not `b` -\> `a`. With this minor change:

```swift
extension BB: Q where T.T.A: Q {}

```

The code does compile.

---

<div class="post-metadata">

**Author:** ![Slava\_Pestov](https://sea2.discourse-cdn.com/swift/user_avatar/forums.swift.org/slava_pestov/32/30204_2.png) [@Slava\_Pestov](https://forums.swift.org/u/Slava_Pestov)\
**Post date:** [May 15, 2023, 11:51pm UTC](https://forums.swift.org/t/two-more-undecidable-problems-in-the-swift-type-system/64814/3 "2023-05-15T23:51:08Z")

</div>

> [@bbrk24](#):
>
> I believe I have found an error in your encoding.

Indeed you’re right, nice catch! Thank you.

---

<div class="post-metadata">

**Author:** ![tera](https://sea2.discourse-cdn.com/swift/user_avatar/forums.swift.org/tera/32/38201_2.png) [@tera](https://forums.swift.org/u/tera)\
**Post date:** [May 16, 2023, 1:09pm UTC](https://forums.swift.org/t/two-more-undecidable-problems-in-the-swift-type-system/64814/4 "2023-05-16T13:09:19Z")

</div>

What is "Smallf%#$\* programming language" ?

---

<div class="post-metadata">

**Author:** ![scanon](https://sea2.discourse-cdn.com/swift/user_avatar/forums.swift.org/scanon/32/2445_2.png) [@scanon](https://forums.swift.org/u/scanon)\
**Post date:** [May 16, 2023, 3:16pm UTC](https://forums.swift.org/t/two-more-undecidable-problems-in-the-swift-type-system/64814/5 "2023-05-16T15:16:18Z")

</div>

A fairly minimal Turing-complete language with a profane name: [Smallf%#$](https://esolangs.org/wiki/Smallfuck)