The Rust type system is indeed turing complete. This has been done.

So obviously I did it again just to see what it took, and to talk a bit on what this implies. Repo is on my Gitea.

The humble cons list

Starting easy, almost trivially if you are used to any functional programming language, with implementing a cons list.

Why do we need a cons list? Well, Rust type system as a programming language is really Lisp-like, and lisp mean cons list.

In common rust, a cons list would look like this:

enum ConsList<T> {
    Cons {
        value: T,
        tail: Box<ConsList<T>>
    },
    Nil
}

But those are runtime values! We are instead going to map this two variant enum into two types:

struct Nil;
struct Cons<Value, Tail>(Value, Tail);

This will map the list [A, B, C] into Cons<A, Cons<B, Cons<C, Nil>>>. This will enable the type system insights into the list content, and damn we will torture that.

The value, or: please extend const generics

The cons list was easy: two values, two types. Brainfuck cells can have 256 value, guess that’s why Shea Leffer used smallfuck. So, we have to define 256 types, to the horror of rustc.

Luckily, Rust has const generics! Here is our value:

struct V<const N: u8>;

and then, obviously, define some associated helpers

trait Value {
    type Next;
    type Prev;
}

impl<const N: u8> Value for V<N> {
    type Next = V<{ N + 1 }>;
    type Prev = V<{ N - 1 }>;
}

aaaand we are informed that generic parameters may not be used in const operations const parameters may only be used as standalone arguments here, i.e. N (rustc). I want to work on the rust compiler at some points, but this looks like something a bit too big to chew.

The result? Macros. I won’t get into the details, it’s quite a boring implementation, relying on a complete list of all possible u8 values. It also implements an empty IsNotZero trait for every type except obviously V<0>. That will be need later!

The tape, and using traits as functions

The tape is now going to be implemented as two lists (the two tails of the tape), and with the current value also, split as a nicety. We will also add two lists, working as the input and output queue.

 struct Tape<Before, Value, After, Input, Output>(Before, Value, After, Input, Output);

Don’t worry about those members: these types are empty, and will never be instantiated!

Then, let’s start actually writing some “code”. The main transformation we will use are traits, and associated types. trait Trait { type Output; } will be our function declaration, and impl Trait for T { type Output = O; } will be the definition Trait(T) = O.

For example, we will define a trait to move the tape left:

/// Return the tape moved to the left
trait GoLeft {
    type Left;
}

// If the tape has values on the left, shift
impl<Before, This, Left, After, Input, Output> GoLeft
    for Tape<Cons<Left, Before>, This, After, Input, Output>
{
    type Left = Tape<Before, Left, Cons<This, After>, Input, Output>;
}
// Else, generate a zero
impl<This, After, Input, Output> GoLeft for Tape<Nil, This, After, Input, Output> {
    type Left = Tape<Nil, V<0>, Cons<This, After>, Input, Output>;
}

Now we can always use <Tape as GoLeft>::Left to get the tape shifted, by popping one element from one tail and pushing the current on the other. GoLeft is implemented in the same way. Plus, hilariously, a so-java-like getter to map the tape to its last parameter, to get out the output at the end.

Instructions: becoming unreadable

Instructions are a two parameter function, meaning a trait with a type parameter other than Self:

trait Instruction<Tape> {
    type Output;
}

Left, Right, Input, Output, Increment, and Decrement are almost trivial to implement, thanks to the previous work. And then there is this one:

struct Loop<Body>(Body);

Linking a [ to a ] was indeed too hard, so I just made it unrepresentable. Of course Body is a list, so we need to implement Instruction for Nil, that’s obviously a no-op, and for Cons<I, T> that’s the composition of the two actions. There types boundary start being a bit longer: you need to ask that:

1. T: Instruction<Tape> as it need to execute first,
2. I: Instruction<<T as Instruction<Tape>>::Output> as it need to execute on the output of the tail.

Implementation for Body is even messier: I had to rewrite a couple of time to get the type checker to comply, as avoiding overlap was quite tricky. For example, using a IsZero trait symmetric to IsNotZero would fail as there might be a type implementing both.

Then there is the type traits on the IsNotZero case, basically unrolling one loop, asking that Cons<Body, Loop<Body>> is a valid instruction, and returning the result of that.

Of course that run in the trap of an infinite loop: that’s a natural cue that indeed the system is turing complete, being required by the halting problem.

Finally, as types are becoming a bit messy, I added a type_fuckery! macro exported at the root of the crate, expanding plain brainfuck and input in a state and a chain of instructions, plus the access to the associated output type. The result is that the macros expands to the cons-list of outputs, except if the program require more input or if the recursion limit is hit.

Why do we even care?

So, why is this even notable? The reason that’s always attached is that this require the Halting problem to be present in the process of type resolution. It requires, indeed, the type system to be able of infinite loops, without any general way of fixing that.

I do not think that’s truly a problem: every example in the repo has a big #![recursion_limit="..."] slapped on top, as even very short program naturally breaks the default one. It is indeed a very obvious way to lower the computational class of a turing complete language.

The main problem I see instead is that turing complete system tend to escape, or at least make extremely difficult, the study of system invariants. Although the sixty-four recursion limits it’s quite generous: in years of rust I hit that only once, outside quite cursed and totally acceptable to reject stuff, and even then it’s easily lifted.

I guess it’s time to find a problem for this solution. Maybe write a transpiler from WASM to Rust types? That would be seriously cursed.