Coq typeclass resolution is Turing-complete

by Thalia Archibald, 15 Apr 2023 The Coq theorem prover has a powerful means of abstraction, typeclasses. To resolve a typeclass instance, the typechecker performs an unrestricted search for an instance satisfying those constraints. The steps in this search resemble the trace of a program execution, and, crucially, it is possible to express unsatisfiable constraints, which cause an infinite search. This indicates it should be Turing-complete! Let's prove it!

Background on typeclasses

A typeclass is essentially an interface associated with a type. Typeclasses were first introduced in Haskell and have since been adopted by many other languages, including in Rust as traits. With its richer dependent types, Coq further extends typeclasses to allow for values in constraints. This allows for computation to be mixed with the search for an instance. For a more in-depth tutorial on typeclasses, see the Typeclasses chapter in the fantastic Software Foundations series. The section on non-termination and the advice from experts are particularly relevant to this.

Smallfuck

To prove Turing-completeness, it is sufficient to implement a Turing-complete language. I model the semantics of Smallfuck, a subset of Brainfuck, using typeclass instances. Smallfuck has a tape of bits and can move the cell pointer left or right, flip the current cell, and loop. I/O and a more complex cell type are not needed to demonstrate Turing-completeness, but you could see how that would be modelled in my bfcoq project. prog represents a Smallfuck program:

• PRight (>) moves the tape right
• PLeft (<) moves the tape left
• PFlip (*) flips the current cell
• PLoop ([…]) repeats while the current cell is 1
• PEnd is a no-op used at the end of a loop or program

tape is an infinite tape, where cell is the current cell and ltape and rtape are the cells to the left and right, respectively.

Let's define a shorthand for booleans.

Big-step semantics

To execute a Smallfuck program, we map an initial tape to a final tape. I model this as a typeclass Exec, that takes a program p and initial and final tapes t and t'. It has a function exec that returns t', so it can be used. Notice that it is parameterized over values p, t, and t', not types. Other languages only allow types as generic parameters, but Coq generalizes it to any dependently-typed term, values and types.

I then define instances of Exec for each operation in big-step semantics style. These define the transformations to be performed in each case, and can be seen as a pattern matching at the instance level. PEnd is the simplest to model; it takes a tape t and maps it to itself (does nothing). Syntactically, this defines an instance named Exec_End, that satisfies Exec for the program PEnd and some tape t for both the initial and final tape.

PFlip negates the current cell. Intuitively, this definition states that if the remainder of the program can be executed, then we can also execute PFlip. That is, if it can resolve an instance for the program starting after applying the flip, then it will supply an instance for the flip. This order is backwards, because it applies the operations post-order in a depth-first search. The parameter `{Exec p t t'} is a class constraint, which implicitly supplies evidence that p t t' has an instance of Exec. It is equivalent to {E : Exec p t t'}, but where the name is not used.

PRight has two cases: When the tape has at least one cell to the left, shift that cell to the current and the old current to the right. When the left tape is empty, use 0 as the new current cell. Here, we destructure Tape, so we can cover the cases of [] and _ :: _.

Likewise for PLeft.

Finally, PLoop has two cases: When the current cell is 0, skip the body and execute the next operation. When the current cell is 1, execute the body, then repeat the loop. Exec_Loop_1 requires two instances, for executing the body once and for executing the loop again.

For comparison, this closely resembles a typical relational definition in Coq, where Exec becomes the type signature and each instance becomes a variant. However, a relation cannot solve for the final tape, like the next section shows with typeclasses.

Execution

Now let's execute programs by typechecking! First, enable typeclass debugging, so we can inspect the search path.

As expected, this typechecks, because > shifts the tape 1(1)01 right to 11(0)1:

However, give it an impossible result and it cannot find an instance:

More usefully, we can generalize it to any tape t and let it infer the final tape after execution:

We can execute loops too, like >*>*[*<]:

Non-terminating programs like [] and >*[>*] work too. For the latter, it cannot resolve an instance for any initial tape. Each iteration of the loop generates for a fresh intermediate value for the tape, which ensures a revisited state will not resolve to the same instance. When no instance can ever satisfy it, which happens for non-terminating programs, the typechecker will infinitely expand the constraints and diverge.

And finally, a program that writes “Hallo, Welt!” in binary to the tape, >*>>>*>>>>>*>*>>>>>*>>*>*>>*>*>>>>*>*>>*>*>>>>*>*>>*>*>*>*>>>*>>*>*>>> >>*>>>>>>>*>>*>>*>*>*>>*>*>>>*>>*>>*>*>>*>*>>>>*>*>*>>*>>>>>*>>>>>*>:

Conclusion

To my knowledge, this is the first proof of the Turing-completeness of typeclass resolution in Coq. You can find the source code for this tutorial at github.com/thaliaarchi/coq-turing-typeclass. For more Turing-complete subsets of programming languages, see my compilation “Unexpectedly Turing-complete”. Thanks for reading!