More precisely, the introduction of SE0142 and SE0157 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 sametype 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 semigroup 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 semigroup 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 semigroups are sufficient for our purposes.
Free semigroups
A free semigroup with generator set G
is the set of all strings formed from the elements of G
. The identity element is the empty string; the semigroup operation is string concatenation.
For example, the free semigroup with a single generator a
contains elements such as 1, a
,aa
, aaa
, etc. This semigroup is isomorphic to the semigroup 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 semigroup with two generators a
and b
has elements that look like this:
abaaa
babbba
abbbabab
Note that unlike the first example, the semigroup operation here is not commutative; for example, ab*b = abb
, but b*ab = bab
.
It is possible to define a free semigroup with infinitely many generators; but for our purposes, let's assume that the generator set is always finite.
Finitelypresented semigroups
We can generalize the notion of finitelygenerated free semigroups by introducing relations.
In a free semigroup, 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 semigroup element. A semigroup with a finite set of generators and relations is called a finitelypresented semigroup.
For example, let's start by taking the free semigroup with two generators a
and b
, and add a relation a*b = b*a
. In this semigroup, 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 semigroup, each element is uniquely determined by the number of a
s and b
s; their relative order does not matter. This semigroup is isomorphic to Z^2
, the semigroup of pairs of integers under pairwise addition.
Here's another example. If we take the free semigroup 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 semigroup is isomorphic to Z/5Z
, the semigroup of integers modulo 5 under addition.
The semigroup of integers under multiplication, on the other hand, is not finitelypresented; the generator set is the set of all prime numbers, which is infinite.
Mapping finitelypresented semigroups 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 SE0157):
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 semigroup with two generators. More precisely, we have a typelevel embedding of the free semigroup with two generators in Swift!
The semigroup elements are type parameters (always prefixed with T.
). The identity element is T
itself.
The semigroup 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 welldefined.
What about finitelypresented semigroups? The free semigroup has no relations, so every string (or type parameter, in our Swift translation) is a unique element (or type).
To map a finitelypresented semigroup 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 semigroup 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 finitelypresented semigroup 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 finitelypresented 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 semigroups with decidable word problems (all the examples we've seen here so far, as well as all finite semigroups, etc), there's no algorithm that will work for an arbitrary finitelypresented semigroup. For example, here is a semigroup 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 SE0142 and SE0157, for that matter).
Clearly, the GenericSignatureBuilder
is able to solve word problems for at least some semigroups today (as well as protocols that don't correspond to semigroups; 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 userwritten 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 SE0142 and SE0157. 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 realworld code. After all, nobody is using Swift for typelevel group theory (yet...).