Swift type checking is undecidable

More precisely, the introduction of SE-0142 and SE-0157 has made canonical type computation into an undecidable problem. I'll begin with the necessary background information before presenting my argument, and then outlining the next steps.

Canonical types

Consider these two protocols, stripped down from the real implementations in the standard library:

protocol IteratorProtocol {
  associatedtype Element
}

protocol Sequence {
  associatedtype Iterator : IteratorProtocol
  associatedtype Element
    where Element == Iterator.Element
  associatedtype SubSequence : Sequence
    where Element == SubSequence.Element, SubSequence.SubSequence == SubSequence
}

We can define a function taking a single generic parameter T constrained to Sequence:

func numberOfElements<T : Sequence>(_ seq: T) -> Int {...}

Inside the function body, the element type of T can be spelled in a number of ways:

T.Element
T.Iterator.Element
T.SubSequence.Element
T.SubSequence.Iterator.Element
T.SubSequence.SubSequence.Element
T.SubSequence.SubSequence.Iterator.Element
...

Indeed, there are infinitely many spellings of T.Element . They are all equivalent, because of the same-type constraints in the Sequence protocol's where clause.

The fact that these equivalent spellings all name the same type is important. Consider a generic function that takes two values of the same, unconstrained generic type:

func isEqual<A>(_: A, _: A) -> Bool

You can call this function with two values that have equivalent types, spelled in two different ways:

let x: T.Element = ...
let y: T.SubSequence.Element = ...

print(isEqual(x, y))

The type checker needs to be able to determine that x and y have the same type, and reject the code if not. This is what we mean by computing canonical types.

Canonical types also important to the ABI; they appear in mangled names, protocol witness table layouts, and other places.

Clearly, computing canonical types is an important operation that we must be able to perform correctly. As you will see below, with the current language, this is impossible in the general case.

Some abstract algebra

A semi-group is a set G , together with a binary operation * . The set contains a distinguished identity element 1, and the binary operation satisfies the following axioms:

a*(b*c) = (a*b)*c
a*1 = 1*a = a

Note that the group operation is not necessarily commutative (that is, a*b != b*a in general).

It is more common to talk about groups in math; a group is a semi-group where each element a has an inverse a^(-1) satisfying a*a^(-1) = a^(-1)*a = 1 . However, we won't need inverses for any of the below, so semi-groups are sufficient for our purposes.

Free semi-groups

A free semi-group with generator set G is the set of all strings formed from the elements of G . The identity element is the empty string; the semi-group operation is string concatenation.

For example, the free semi-group with a single generator a contains elements such as 1, a , aa , aaa , etc. This semi-group is isomorphic to the semi-group of integers under addition. The isomorphism is defined as the length of the string; this is an isomorphism since the length of the concatenation of two strings is the sum of the lengths of the individual strings.

A free semi-group with two generators a and b has elements that look like this:

abaaa
babbba
abbbabab

Note that unlike the first example, the semi-group operation here is not commutative; for example, ab*b = abb , but b*ab = bab .

It is possible to define a free semi-group with infinitely many generators; but for our purposes, let's assume that the generator set is always finite.

Finitely-presented semi-groups

We can generalize the notion of finitely-generated free semi-groups by introducing relations .

In a free semi-group, each string formed from the generator elements denotes a unique element. Relations, on the other hand, define an eqivalence, stipulating that two different spellings name the same semi-group element. A semi-group with a finite set of generators and relations is called a finitely-presented semi-group .

For example, let's start by taking the free semi-group with two generators a and b , and add a relation a*b = b*a . In this semi-group, when you apply the binary operation to two elements, say abba and bbab , you first concatenate the strings to form abbabbab , but then you can make use of the relation a*b = b*a to swap adjacent a s and b s until all a s appear at the beginning of the string and all b s at the end. In our example this gives us aaabbbbb . This means that in this semi-group, each element is uniquely determined by the number of a s and b s; their relative order does not matter. This semi-group is isomorphic to Z^2 , the semi-group of pairs of integers under pair-wise addition.

Here's another example. If we take the free semi-group with one generator a and add a relation a*a*a*a*a = 1 , we get a finite group. There are only 5 elements in total, and this semi-group is isomorphic to Z/5Z , the semi-group of integers modulo 5 under addition.

The semi-group of integers under multiplication, on the other hand, is not finitely-presented; the generator set is the set of all prime numbers, which is infinite.

Mapping finitely-presented semi-groups to protocols

So what does all of this mean? Let's define a protocol with two associated types, where each associated type conforms to the protocol recursively (that's SE-0157):

protocol P {
  associatedtype A : P
  associatedtype B : P
)

If you define a function with a generic parameter constrained to P , the type parameters you can write in the function's body are all the strings formed from the associated types A and B :

func foo<T : P>(_: T) {
  let x: T = ...
  let y: T.A = ...
  let z: T.B.A.B = ...
}

If this looks familiar, it's because this is in fact the free semi-group with two generators. More precisely, we have a type-level embedding of the free semi-group with two generators in Swift!

The semi-group elements are type parameters (always prefixed with T. ). The identity element is T itself.

The semi-group operation is concatenation. Since both associated types conform to P , every type parameter you can write here conforms to P , which makes this concatenation operation well-defined.

What about finitely-presented semi-groups? The free semi-group has no relations, so every string (or type parameter, in our Swift translation) is a unique element (or type).

To map a finitely-presented semi-group with relations to Swift, we need to encode the relations in the form of a where clause on the protocol. For example, here is our previous example of the semi-group of integers modulo 5, encoded in Swift:

protocol Z5 {
  associatedtype A : Z5
    where A.A.A.A.A == Self
}

If you define a function to have a generic parameter T constrained to Z5 , you can write the following types in the function body:

T
T.A
T.A.A
T.A.A.A
T.A.A.A.A

These are all the unique types here. All longer types are equivalent to one of the above. For example, the type checker can prove that T.A.A.A.A.A.A is equivalent to T.A .

We're almost ready to look at the undecidability argument. It all rests on the above encoding of a finitely-presented semi-group as a Swift protocol. If I made a mistake in the above, then none of what follows is valid!

The word problem

The word problem on finitely-presented groups asks if two strings of generators denote the same element. The word problem is known to be undecidable in the general case.

While there are plenty of examples of semi-groups with decidable word problems (all the examples we've seen here so far, as well as all finite semi-groups, etc), there's no algorithm that will work for an arbitrary finitely-presented semi-group. For example, here is a semi-group with an undecidable problem:

Generators: a, b, c, d, e
Relations:
- ac = ca
- bc = cb
- bd = db
- ce = eca
- de = edb
- cca = ccae

We can translate this to Swift as above by mapping generators to associated types and relations to where clause entries:

protocol Impossible {
  associatedtype A : Impossible
  associatedtype B : Impossible
  associatedtype C : Impossible
  associatedtype D : Impossible
  associatedtype E : Impossible
    where A.C == C.A
          A.D == D.A
          B.C == C.B
          B.D == D.B
          C.E == E.C.A
          D.E == E.D.B
          C.C.A == C.C.A.E
}

Cupertino, we have a problem. We can write down a Swift protocol -- using our existing language features -- where computing canonical types is known to be undecidable.

What does this mean?

Well, it's not the end of the world (or the end of Swift, or even the end of SE-0142 and SE-0157, for that matter).

Clearly, the GenericSignatureBuilder is able to solve word problems for at least some semi-groups today (as well as protocols that don't correspond to semi-groups; which is any protocol that has at least one associated type that does not conform to the protocol recursively). After all, the standard library and a large amount of user-written code makes use of generics, and works correctly.

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.

What we need to do is come up with an appropriate restriction to the combination of SE-0142 and SE-0157. If a protocol obeys the restriction, the algorithm should always terminate with the correct result. If a protocol does not obey the restriction, we want to be able to produce a diagnostic instead of crashing or miscompiling.

I'm optimistic that introducing this restriction should have very little impact on real-world code. After all, nobody is using Swift for type-level group theory (yet...).

References

• SE-0142
• SE-0157
• Wikipedia
• A simple presentation of a group with unsolvable word problem

Swift already stops compiling if too much time is required to correctly infer the type of a variable. Moreover, your proposed example won't work since Swift fails to correctly constrain the associated type:

protocol Z5 {
    associatedtype A: Z5 where A.A.A.A.A == Self
}

extension Int: Z5 {
    typealias A = Double
}

extension Double: Z5 {
    typealias A = Float
}

extension Float: Z5 {
    typealias A = String
}

extension String: Z5 {
    typealias A = UInt
}

extension UInt: Z5 {
    typealias A = UInt32  // UInt shouldn't conform, but it (wrongly) does
}

extension UInt32: Z5 {
    typealias A = UInt16
}

extension UInt16: Z5 {
    typealias A = Int32
}

extension Int32: Z5 {
    typealias A = Int64
}

extension Int64: Z5 {
    typealias A = Int
}

func f<T: Z5>(_ x: T) {
    print(T.self)
    print(T.A.self)
    print(T.A.A.self)
    print(T.A.A.A.self)
    print(T.A.A.A.A.self)
    print(T.A.A.A.A.A.self)
    print(T.A.A.A.A.A.A.self)
    print(T.A.A.A.A.A.A.A.self)
}

f(0)

// Prints the following:
//
// Int
// Double
// Float
// String
// UInt
// UInt32
// UInt16
// Int32

Thanks for the very understandable construction, Slava! Did you have a particular set of restrictions in mind?

The obvious and easy ways to restrict things in the compiler are via limiting (1) the number of generators, (2) the number of relations, and/or (3) the length of the relations.

The Impossible protocol has 5 generators and 7 relations, with a max length of 3. The paper you reference also mentions a result by Ju.V. Matijasevic with only 3 relations, but one of them has a length of "several hundred occurrences of generators".

I don't think that there is anything in the standard library that has more than 1 generator (a protocol with an associated type recursive with itself). Is it too limiting to make recursion (in the SE-0157 sense) only able to happen on a single associated type (extremely simple to understand and diagnose)?

Alternately, is it possible to build an undecidable protocol if relations can't refer to more than one generator? I.e. we would allow Z5 but not theoretical protocols with multiple generators with where clauses that refer to other generators:

protocol Allowed {
    associatedtype A : Allowed
    associatedtype B : Allowed where B.B == B
}

protocol NotAllowed {
    associatedtype A : NotAllowed
    associatedtype B : NotAllowed where B.A == B
}

(Obviously my bias here is towards the goal of chopping off undecidability and of ease of explaining what the rules are in the resulting error messages, as opposed to trying to allow the maximum possible amount of decidable type-level group theory.)

Hmm... what version of Swift were you using? 5.3 rejects the code:

g.swift:21:1: error: type 'UInt' does not conform to protocol 'Z5'
extension UInt: Z5 {
^
g.swift:22:15: note: possibly intended match 'UInt.A' (aka 'UInt32') does not conform to 'Z5'
    typealias A = UInt32  // UInt shouldn't conform, but it (wrongly) does
              ^
g.swift:2:20: note: protocol requires nested type 'A'; do you want to add it?
    associatedtype A: Z5 where A.A.A.A.A == Self
                   ^