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 (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...).

References

100 Likes

I love your rigor on this topic. I was surprised when recursive protocol constraints worked at all in Swift 4.1; I'm less surprised that some limits might need to be imposed.

11 Likes
Off topic

:eyes: (an excerpt from my old github)

public protocol BasisChain {
    associatedtype Next: BasisChain
}
public enum EndBasisChain: BasisChain {
    public typealias Next = Self
}
public enum BasisLink<Current: Basis, Next: BasisChain>: BasisChain { }

At some point, I need the compiler needs to prove that BaseLink<BaseLink<BaseLink<BaseLink<Empty>>>>.Next.Next.Next == BaseLink<BaseLink<BaseLink<Empty>>>>.Next.Next and it just broke. So I did a major refactoring anyway~

4 Likes

What an excellent post; thank you @Slava_Pestov for writing this up and explaining the problem so clearly!

Do you have any initial ideas from the mathematical literature about what sort of restriction we may want to pursue here? Also, semi-groups are one model where this undecidability problem is exhibited—how should we evaluate a proposed restriction to make sure that it attacks all other decidability issues in addition to the semi-group modeling one?

3 Likes

Great work Slava!

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
Mathematical off topic

May I suggest a couple corrections?

It would've been if you considered the group. Without the inverses you can't build an isomorphism to \mathbb{Z}\times\mathbb{Z} ;)

The last type should actually be equal to T, it should be removed from the list :)

2 Likes

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.)

2 Likes

The difficulty here is that we still have to come up with an algorithm that works within these restrictions. Also they might not be sufficient. A protocol with self-recursive associated types is one way we can express an undecidable problem, but there are others. For example, you can have multiple mutually-recursive protocols.

I would instead look for some kind of condition on the types written in the relations themselves, but honestly I haven't thought about it very deeply yet.

It would be nice if we could restrict recursive conformances to generate a finite set of unique type parameters by using a where clause that introduces a "loop" in the graph, like we do with Sequence.SubSequence, or in Z5 in my example, but I fear that's not going to be good enough and will break a lot of existing code.

5 Likes

Intuitively, what you want is a rewrite system where you can always limit yourself to applying rewrite rules that make a type shorter. You should never have to 'expand' it to make it longer because you need to apply some other simplification. I'm not sure how to formalize -- or explain this in diagnostics -- just yet.

4 Likes

Right, the theoretical issues are essentially moot. We just need an algorithm that doesn’t produce wrong answers. It’s fine if there are some cases it can’t solve—those ought to raise a “too complex” diagnostic.

2 Likes

That's quite different. As far as I know, the constraint solver should eventually terminate, however it might take a long time because of exponential blowup.

That's a bug... I'll make a note of it to look at later.

1 Like

There is an argument to be made that such code is already kind of broken, if only because of the difficulty of reasoning about it. E.g., Collection is missing an Indices.Indices == Indices clause, the consequences of which I find really difficult to grasp.

4 Likes

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
                   ^

Which is sufficient to improve the diagnostics here - since we should be able to signal to the user when the GSB gets "stuck" on a term. A more general answer to the word problem will involve distilling something about the many many classes of groups where the word problem is not just solvable, but decidably so.

There's also a lot of literature on rewrite systems that will promise you nice properties if you trade away expressiveness in the underlying language. Knuth-Bendix is one of the more famous algorithms here.

2 Likes

I've had an intuitive feeling that this was true for a long time, but I never put together a good proof of it; nice work.

11 Likes

I had just posted this apparent compiler bug: https://bugs.swift.org/browse/SR-13341 when I stumbled upon this post, and I'm curious if it happens to be an example of the failure to canonicalize that you're talking about. My compiler knowledge is poor, so I apologize if this is in reality quite unrelated to what you're talking about.

Well done! I'm wondering about the undecidability property here. I know that the halting problem proof rests in diagonalization. So, given any particular program on a particular computer I can decide if it halts; I just need an exponentially bigger computer to run exponentially longer and map out all the state transitions.

Is it true that things are different here? That is, is there some particular finite-sized group for which there exists a finitely-sized member which is undecidable? In other words, can I write a (finite) Swift program that is undecidable? It feels like, for any finitely-sized case, an algorithm ought to be able to run through every possible sequence of generators and relations till the space repeats. But I'm probably missing something.

Very cool!

1 Like

I'm running Swift 5.3 from a Playground, in Xcode 12 beta 3 (12A8169g).

Uhh, small point. When you say:

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)

Correct me if I'm wrong, but I believe that is a monoid, not a semigroup. A semigroup does not require an identity element, and a monoid Is exactly the triple (G, *, I).

Otherwise, this is a very interesting problem to overcome. Yet another unsound type system? hehehe

5 Likes

Yet another unsound type system?

Let's put a fine point on this: Decidability and soundness are two distinct properties when talking about type systems. It is perfectly valid to have undecidable type checking/synthesis but still have a system that is sound. Most (dependent) type theories that carry an extensional equality fit this bill - though Epigram's observational type theory holds a special place in my heart because its propositional equality is extensional, yet type checking is still decidable. Type Inference in System F is also undecidable (don't confuse this with type checking, which is decidable), but variants of that system form the basis of Haskell and many many flavors of ML.

18 Likes
Terms of Service

Privacy Policy

Cookie Policy