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(associativity) -
a*1 = 1*a = a(identity)
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 as and bs until all as appear at the beginning of the string and all bs 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 as and bs; 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...).
(an excerpt from my old 