(N.B. The word “fuck” appears multiple times in this post. I recommend that the reader temporarily not consider “fuck” as profanity, as it isn’t used that way here.)

Not so long ago, a certain someone made a challenge on the Rust subreddit asserting that while everyone likes to say that Rust’s type system is Turing-complete, no one actually seems to have a proof anywhere. In response to that post, I constructed a proof in the form of an implementation of Smallfuck – a known Turing-complete language – entirely in the Rust type system. This blog post is an attempt to explain the inner workings of that Smallfuck implementation, as while as what this means for the Rust type system.

So what is Turing-completeness? Turing-completeness is a property of most programming languages which states that they can simulate a universal Turing machine. A related notion is Turing-equivalence. Turing-equivalent languages can simulate and be simulated by Turing-machines – so if you have any two Turing-equivalent languages, it must be possible to translate any program written for one into a program written for the other. Most if not all Turing-complete systems are also known to be Turing-equivalent. (I regret not being able to find a better citation for this.)

There are several important things to note about Turing-completeness. We know about the halting problem. One consequence of this is that if you have a Turing-complete language, which can simulate any universal Turing machine, then it must be capable of infinite loops. This is why it’s useful to know whether or not Rust’s type system is Turing-complete – what that means is, if you’re able to encode a Turing-complete language into Rust’s type system, then the process of checking a Rust program to ensure that it is well-typed must be undecidable. The typechecker must be capable of infinite loops.

How do we show that the Rust type system is Turing-complete? The most straightforward way to do so (and in fact I don’t know of any other ways) is to implement a known Turing-complete language in it. If you can implement a Turing-complete language in another language, then you can clearly simulate any universal Turing machine in it – by simulating it in the embedded language.

Smallfuck: Useless and Useful

So, what’s Smallfuck? Smallfuck is a minimalist programming language which is known to be Turing-complete when memory restrictions are lifted. I chose it to implement in the Rust type system over other Turing-complete languages because of its simplicity. While esoteric languages are fairly useless for actually writing programs, they’re great for proving Turing-completeness.

Smallfuck is actually pretty close to a Turing machine itself. The original specification for Smallfuck states that it runs in a machine with a finite amount of memory. However, if we lift that restriction and allow it to access a theoretically infinite array of memory, then Smallfuck becomes Turing-complete. So here, we consider a variation of Smallfuck with infinite memory. The Smallfuck machine consists of an infinite tape of memory consisting of “cells” containing bits along with a pointer into that array of cells.

                 Pointer |
                         v
...000001000111000001000001111...

Smallfuck programs are strings of five instructions:

< | Pointer decrement
> | Pointer increment
* | Flip current bit
[ | If current bit is 0, jump past the matching ]; else, go to the next instruction
] | Jump back to the matching [ instruction

This gives you the ability to select cells and make loops. Here’s a simple example program:

>*>*>*[*<]

This is a dead simple and totally useless program (as most programs are in Smallfuck, thanks to its total lack of any sort of I/O whatsoever) which simply sets three bits in a row to 1, and then uses a loop to put them all back to 0, ending with the pointer in the same location it started. A visualization:

Instruction pointer
|               Memory pointer
v               v
>*>*>*[*<] | ...0...

The first instruction moves the pointer to the right. All cells default to 0:

 v               v
>*>*>*[*<] | ...00...

The next instruction is a “flip current bit” instruction, so we flip the bit at the pointer from 0 to 1.

 v               v
>*>*>*[*<] | ...01...

This occurs three times. Let’s skip ahead to the start of the loop:

      v            v
>*>*>*[*<] | ...0111...

Now we’re at the beginning of a loop. The [ instruction says, “if the current bit is zero, jump to the matching ]; else, go to the next instruction.” The bit at the pointer is 1, so we go to the next instruction.

       v           v
>*>*>*[*<] | ...0111...

This flips the current bit back to zero; then, we move the memory pointer back one location.

         v        v
>*>*>*[*<] | ...0110...

Now we’re at the closing ]. This is an unconditional jump back to the start of the loop.

      v           v
>*>*>*[*<] | ...0110...

Now we branch again. Is the current cell zero? No? Then we continue:

       v          v
>*>*>*[*<] | ...0110...

        v         v
>*>*>*[*<] | ...0100...

         v       v
>*>*>*[*<] | ...0100...

      v          v
>*>*>*[*<] | ...0100...

After looping one last time, we end up here:

      v         v
>*>*>*[*<] | ...0000...

Which is exactly where we started: all cells back to zero, and with the pointer in its starting location.

Runtime Smallfuck in Rust

So what would a simple implementation of this look like in Rust? I’ll start by walking through the run-time implementation of Smallfuck that I bundled with my type-level implementation in order to verify that the type-level and run-time implementations coincided. We’ll store Smallfuck programs as an AST, like so:

enum Program {
    Empty,
    Left(Box<Program>),
    Right(Box<Program>),
    Flip(Box<Program>),
    Loop(Box<(Program, Program)>),
}

This isn’t quite true to the representation of Smallfuck as a string, but it’s much easier to interpret. We also need a type to represent the state of a running Smallfuck program:

struct State {
    ptr: u16,
    bits: [u8; (std::u16::MAX as usize + 1) / 8],
}

Although to be Turing-complete we technically need an infinite tape, this run-time implementation is only for checking the semantics of the type-level version. A finite tape is a perfectly fine approximation to make, for now. By making the length of bits to be (std::u16::MAX + 1) / 8, we ensure that we have a bit for every u16 address. Now for some operations which we’ll use in implementing our interpreter:

impl State {
    fn get_bit(&self, at: u16) -> bool {
        self.bits[(at >> 3) as usize] & (0x1 << (at & 0x7)) != 0
    }

    fn get_current_bit(&self) -> bool {
        self.get_bit(self.ptr)
    }

    fn flip_current_bit(&mut self) {
        self.bits[(self.ptr >> 3) as usize] ^= 0x1 << (self.ptr & 0x7);
    }
}

This is some fairly standard bit manipulation. We store 8 bits into one cell in our bits array, so to find out which cell a given bit goes to, we use truncating division by 8, which if we’re trying to be exceedingly clever results in a bit-shift to the right by three places. We’re essentially using this addressing scheme, where the lower three bits of the u16 pointer indicate the bit of the byte in bits, and the higher 13 bits indicate the index of the byte in bits:

Index into the bytes of `bits` --> 1100011010011 \ 001 <-- Which bit in the byte

So it’s clear we can do things through nice little bit-masks. Shifting right by three places chops off the “which bit” section, leaving just the index. 0x7 in hexadecimal is 0b111 in binary. This makes its purpose quite clear: taking & 0x7 clears all bits in our pointer except for the last three, which indicate which bit in the byte. Shifting 0x1 by that amount gets us a u8 with only a single bit set to 1, letting us index our byte; and finally, != 0 lets us quickly check whether or not the respective bit is set. The xor operation in flip_current_bit simply flips the indexed bit.

Now that we have those primitives, let’s move on to implementing our interpreter. We’ll do so by recursively calling a function which pattern-matches over Program:

impl Program {
    fn big_step(&self, state: &mut State) {
        use self::Program::*;

        match *self {
            Empty => unimplemented!(),
            Left(ref next) => unimplemented!(),
            Right(ref next) => unimplemented!(),
            Flip(ref next) => unimplemented!(),
            Loop(ref body_and_next) => unimplemented!(),
        }
    }
}

An Empty program modifies no state, so its implementation is very simple:

Empty => {},

Left and Right just increment/decrement the pointer by one. Since we’ve chosen to use a wrapping tape in our simple implementation, we use wrapping_add and wrapping_sub:

Left(ref next) => {
    state.ptr = state.ptr.wrapping_sub(1);
    next.big_step(state);
},
Right(ref next) => {
    state.ptr = state.ptr.wrapping_add(1);
    next.big_step(state);
},

Flip is very simple, since we wrote our convenient flip_current_bit function:

Flip(ref next) => {
    state.flip_current_bit();
    next.big_step(state);
},

And last but not least, Loop. We check the current bit. If it’s 1, then we execute the body of the loop, and then execute the loop instruction again with the updated state. If it’s 0, we move on to the next instruction:

Loop(ref body_and_next) => {
    let (ref body, ref next) = **body_and_next;
    if state.get_current_bit() {
        body.big_step(state);
        self.big_step(state);
    } else {
        next.big_step(state);
    }
},

We have to do the double-deref on body_and_next because we boxed the tuple. We avoid moving out of the box by binding by ref. Our finished .big_step() function looks like this:

impl Program {
    fn big_step(&self, state: &mut State) {
        use self::Program::*;
    
        match *self {
            Empty => {},
            Left(ref next) => {
                state.ptr = state.ptr.wrapping_sub(1);
                next.big_step(state);
            },
            Right(ref next) => {
                state.ptr = state.ptr.wrapping_add(1);
                next.big_step(state);
            },
            Flip(ref next) => {
                state.flip_current_bit();
                next.big_step(state);
            },
            Loop(ref body_and_next) => {
                let (ref body, ref next) = **body_and_next;
                if state.get_current_bit() {
                    body.big_step(state);
                    self.big_step(state);
                } else {
                    next.big_step(state);
                }
            },
        }
    }
}

We won’t be implementing any sort of debug printing for our State since we won’t need it. When we use our run-time interpreter to check against our type-level interpreter, we’ll do so by iterating over the bits in the output of the type-level interpreter and checking to ensure that the same bits are set in the run-time output. Now, we’re free to start on the fun stuff!

Type-Level Smallfuck in Rust

Rust has a feature called traits. Traits are a way of doing compile-time static dispatch, and can also be used to do runtime dispatch (although in practice that’s rarely useful.) I will assume here that the reader knows what traits are in Rust and has used them a fair amount. To implement Smallfuck, we’ll be relying on a particular feature of traits known as associated types.

Trait resolution and unification

In Rust, in order to call a trait method or resolve an associated type, the compiler must go through a process called trait resolution. In order to resolve a trait, the compiler has to look for an impl which unifies with the types involved. Unification is a process for solving equations between types. If there is no solution, we say that unification has failed. Here’s an example:

trait Foo<B> {
   type Associated;
}


impl<B> Foo<B> for u16 {
    type Associated = bool;
}


impl Foo<u64> for u8 {
    type Associated = String;
}

This is a very contrived example, but it will serve a point. In order to resolve a reference to an associated type (e.g. <F as Foo<T>>::Associated), the Rust compiler has to search for an impl which matches F and T correctly. Let’s say that we have F == u16 and T == u64. What if the compiler tries the second impl, of Foo<u64> for u8? Then it will immediately find that F does not match u8 – so, it’s not the impl we’re looking for. What if it tries the first? Then we have F == u16, which is true, so all good. Now we have to match T == B. And here’s where the magic happens.

The Rust compiler unifies F with B. Since B is a type variable – not a concrete type, like String or u64 – its value is free to be assigned. So now B is replaced with u64, and going through with the substitution of B => u64, we now have an impl of Foo<u64> for u16 which is valid. Unification is a fairly simple procedure: it takes in a type (term) which may have variables, and every time it runs into a place where a variable that hasn’t yet been assigned is matched against any other term, the variable is assigned to that term (even if the other term is a variable!) Then, any time that variable is come across while unifying the same term, it’s replaced with its assigned value, and instead unification tries to unify the assigned value against the other term.

The output of unification is a “substitution” - a mapping of variables to terms, such that when you take the terms you were trying to unify and replace all the variables mentioned in the substitution with the terms they’re mapped to, you end up with two identical terms. Here’s a standalone example of unification, trying to unify Foo<X, Bar<u16, Z> with Foo<Baz, Y>:

Foo<X, Bar<u16, Z>> == Foo<Baz, Y>

First we check the heads of the terms - we get Foo vs. Foo, which checks out. So we haven’t failed to unify yet. If we had, say, Foo == Bar, then unification would fail. Next, we decompose this into two subproblems. We know Foo<A, B> == Foo<C, D> if and only if A == C and B == D:

X == Baz, Bar<u16, Z> == Y

We’ve now solved a variable – X has a clearly defined value, Baz. So we can now add to our substitution, [X -> Baz]. Then, we apply that substitution to the second term, Bar<u16, Z> == Y. Since there are no occurrences of X in there, nothing happens, and we’re left with the same term. And then we have a solution for Y. So our final substitution looks like [X -> Baz, Y -> Bar<u16, Z>]. Let’s observe what happens when we apply that to the original equation we wanted to check:

Foo<X, Bar<u16, Z>> == Foo<Baz, Y> [X -> Baz, Y -> Bar<u16, Z>]

Becomes:

Foo<Baz, Bar<u16, Z>> == Foo<Baz, Bar<u16, Z>>

Which is obviously true. The two terms are now equal! So what’s an example of unification failing? Let’s try:

Foo<Bar, X> == Foo<X, Baz>

Which breaks down into two equations:

Bar == X, X == Baz

So we solve the first equation, obtaining the substitution [X -> Bar]. Applying this to X == Baz yields Bar == Baz, which is clearly false. So our unification has failed – there isn’t a solution.

Unification is such a useful process that there actually exists a programming language, Prolog, which describes programs through logical terms, and execution is unification of terms. So that seems suspicious. If you have a Turing-complete language, Prolog, which is based off of unification, then it seems straightforward that Rust’s trait resolution – which works by attempting to unify trait impls until it finds the one which works – might be Turing-complete as well.

Computing with traits

And now that we’ve got the boilerplate out of the way, let’s look at how we actually write this in Rust. We’ll start our Smallfuck implementation now! We’ll be using a macro I wrote a few months ago called type_operators! which compiles a DSL into a collection of Rust struct definitions, trait definitions, and trait impls. While I’ll be explaining my implementation using type_operators!, I’ll also be showing what the type_operators! invocations expand to. Let’s get started!

We’ll start simple. How do we represent the bits of our Smallfuck state in Rust types?

type_operators! {
    [ZZ, ZZZ, ZZZZ, ZZZZZ, ZZZZZZ]
    
    concrete Bit => bool {
        F => false,
        T => true,
    }
}

There are several things to note here. The first is the weird list, [ZZ, ZZZ, ZZZZ, ZZZZZ, ZZZZZZ]. That one’s hard to explain, but it has to do with how Rust macros can’t create unique type names. So you have to get around this with a hack where you provide your own list. Ignore this for now - it’s not related to the actual implementation. But, concrete Bit is!

type_operators! takes two kinds of type-level pseudo-datatype definitions - data and concrete. The difference lies in how type_operators! generates traits to ensure you don’t mismatch these type-level datatypes. The above example compiles to the following definitions:

pub trait Bit {
    fn reify() -> bool;
}


pub struct T;
pub struct F;


impl Bit for T {
    fn reify() -> bool { true }
}

impl Bit for F {
    fn reify() -> bool { false }
}

Hopefully you can now see what’s happening! T and F become unit structs implementing Bit. Bit gives them a reify() function that lets you turn the types T and F into the corresponding boolean representation. So you can write <T as Bit>::reify() which will produce true. This is useful because then as long as you have a type variable B: Bit, you can use B::reify() to turn it into a boolean. I use this for turning the output of the Smallfuck interpreter into values that I can check against the runtime implementation.

Hopefully that was fairly clear! Let’s look another concrete definition we have:

concrete List => BitVec {
    Nil => BitVec::new(),
    Cons(B: Bit, L: List = Nil) => { let mut tail = L; tail.push(B); tail },
}

Now… we have some complexity. Let’s dig through this slowly.

This is a type-level cons-list. The first thing we get out of this is a pair of struct types, Nil and Cons:

pub struct Nil;
pub struct Cons<B: Bit, L: List = Nil>(PhantomData<(B, L)>);

So now we’ve got bits and lists of bits. We can construct a list [T, F, F] as Cons<T, Cons<F, Cons<F, Nil>>>. We also get some traits on top of this:

pub trait List {
    fn reify() -> BitVec;
}


impl List for Nil {
    fn reify() -> BitVec { BitVec::new() }
}

impl<B: Bit, L: List> List for Cons<B, L> {
    fn reify() -> BitVec {
        let mut tail = <L as List>::reify();
        tail.push(<B as Bit>::reify());
        tail
    }
}

So one thing to note is that

Cons(B: Bit, L: List = Nil) => { let mut tail = L; tail.push(B); tail }

results in a sort of syntax sugar where L and B are automatically reified and then bound into those variables. This is to get around some limitations of macro hygiene, and to allow the user to actually use those values.

So hopefully now that you’ve got that all figured out, let’s examine the last two concrete definitions we’ll be using:

concrete ProgramTy => Program {
    Empty => Program::Empty,
    Left(P: ProgramTy = Empty) => Program::Left(Box::new(P)),
    Right(P: ProgramTy = Empty) => Program::Right(Box::new(P)),
    Flip(P: ProgramTy = Empty) => Program::Flip(Box::new(P)),
    Loop(P: ProgramTy = Empty, Q: ProgramTy = Empty) => Program::Loop(Box::new((P, Q))),
}

concrete StateTy => StateTyOut {
    St(L: List, C: Bit, R: List) => {
        let mut bits = L;
        let loc = bits.len();
        bits.push(C);
        bits.extend(R.into_iter().rev());

        StateTyOut {
            loc: loc,
            bits: bits,
        }
    },
}

Hopefully you’ve got all the patterns figured out by now. Here’s a complete listing showing how all these definitions compile down to Rust structs, traits, and impls:

The ProgramTy is fairly straightforward, and hopefully you can now see why I chose to encode the run-time encoding of Smallfuck programs as an AST – to mirror the type-level encoding as best as possible. The St type under the StateTy trait is a zipper list representing simultaneously the pointer location and memory of the Smallfuck interpreter. The L and R lists represent the memory to either side of C, the current bit under the pointer.

Now we can look at the most interesting part – the actual implementation of the Smallfuck interpreter. It consists of one trait and a dozen or so impls. Here’s the type_operators! code:

(Run) Running(ProgramTy, StateTy): StateTy {
    forall (P: ProgramTy, C: Bit, R: List) {
        [(Left P), (St Nil C R)] => (# P (St Nil F (Cons C R)))
    }
    forall (P: ProgramTy, L: List, C: Bit) {
        [(Right P), (St L C Nil)] => (# P (St (Cons C L) F Nil))
    }
    forall (P: ProgramTy, L: List, C: Bit, N: Bit, R: List) {
        [(Left P), (St (Cons N L) C R)] => (# P (St L N (Cons C R)))
        [(Right P), (St L C (Cons N R))] => (# P (St (Cons C L) N R))
    }
    forall (P: ProgramTy, L: List, R: List) {
        [(Flip P), (St L F R)] => (# P (St L T R))
        [(Flip P), (St L T R)] => (# P (St L F R))
    }
    forall (P: ProgramTy, Q: ProgramTy, L: List, R: List) {
        [(Loop P Q), (St L F R)] => (# Q (St L F R))
        [(Loop P Q), (St L T R)] => (# (Loop P Q) (# P (St L T R)))
    }
    forall (S: StateTy) {
        [Empty, S] => S
    }
}

This compiles to a whole lotta stuff. The first thing is a trait. Here’s where that weird gensym list comes into play. Since the gensyms are only used here, they can’t collide with anything the user writes since nothing involving type variables are actually spliced in. Since writing ZZ, ZZZ etc. is a pain, I’m going to ignore what I actually put in that gensym list and just write nicely:

pub trait Running<S: StateTy>: ProgramTy {
    type Output: StateTy;
}

pub type Run<P: ProgramTy, S: StateTy> = <P as Running<S>>::Output;

So, (Run) Running(ProgramTy, StateTy): StateTy becomes a sort of type-level function from two types implementing ProgramTy and StateTy respectively and ouputting one type which implements StateTy. Now for the stuff inside. Let’s take a look at one simple definition:

forall (P: ProgramTy, C: Bit, R: List) {
    [(Left P), (St Nil C R)] => (# P (St Nil F (Cons C R)))
}

This compiles down to a trait impl, like so:

impl<P: ProgramTy, C: Bit, R: List> Running<St<Nil, C, R>> for Left<P>
    where P: Running<St<Nil, F, Cons<C, R>>> {
    type Output = <P as Running<St<Nil, F, Cons<C, R>>>>::Output;
}

The (# P (St Nil F (Cons C R))) means “recursively ‘call’ the type-level function with the arguments P (St Nil F (Cons C R)).” type_operators! uses a lisp-like DSL for ease of parsing; (A B C) compiles to the type A<B, C>. The # “function” is special in type_operators! because its usage must be tracked: whenever a call to # is made, an additional constraint must be added to the where clause. You can see how this works in the example above.

Now that the semantics of the type-level function definition are clarified, let’s look at how Smallfuck is defined. We have four different definitions which deal with the Left and Right instructions:

forall (P: ProgramTy, C: Bit, R: List) {
    [(Left P), (St Nil C R)] => (# P (St Nil F (Cons C R)))
}
forall (P: ProgramTy, L: List, C: Bit) {
    [(Right P), (St L C Nil)] => (# P (St (Cons C L) F Nil))
}
forall (P: ProgramTy, L: List, C: Bit, N: Bit, R: List) {
    [(Left P), (St (Cons N L) C R)] => (# P (St L N (Cons C R)))
    [(Right P), (St L C (Cons N R))] => (# P (St (Cons C L) N R))
}

The first one defines what occurs when the pointer moves left, but the left-hand cons-list in our zipper list is empty. We have to create a new F bit, and move the current bit into the right-hand side cons-list. The left-hand cons list stays Nil. The second definition here works equivalently, but in the case that the pointer has to move right yet the right-hand cons-list is Nil. The third and fourth definitions, respectively, deal with the cases where the left and right cons-lists are Cons<N, L> and Cons<N, R> respectively. In this case, we can pop the next value out of the cons-list and move it to be the current bit; and then push the current bit back into the other cons-list. Here’s a better visualization:

The zipper list is like this:
[...L...] C [...R...]
Where ...L... represents a list which may be Cons or Nil; we don't care. It's
opaque.

[...L..., LN] C [RN, ...R...]
Here is a list where the left-hand list is Cons<LN, L> and the right-hand list
is Cons<RN, R>.

The variables used here are meaningful: L = Left, R = Right, N = Next, C = Current.

Pointer moves left, left-hand side is Nil:
[] C [...R...] => [] 0 [C, ...R...]

Pointer moves right, right-hand side is Nil:
[...L...] C [] => [...L..., C] 0 []

Pointer moves left, left-hand side is Cons<N, L>:
[...L..., N] C [...R...] => [...L...] N [C, ...R...]

Pointer moves right, right-hand side is Cons<N, R>:
[...L...] C [N, ...R...] => [...L..., C] N [...R...]

So how does Rust actually “execute” these left and and right movements? Let’s say we have a current program Left<P> and a state St<Nil, F, R>. When we put these into the Run<P, S> type synonym as Run<Left<P>, St<Nil, F, R>> we end up with <Left<P> as Running<St<Nil, F, R>>>::Output. This causes Rust to look for impls to unify.

Due to Rust’s rules for writing traits and impls, there can only ever be at most one valid impl for any given types Rust attempts to find an impl for. Rust finds the impl that we compiled by-hand as an example earlier:

impl<P: ProgramTy, C: Bit, R: List> Running<St<Nil, C, R>> for Left<P>
    where P: Running<St<Nil, F, Cons<C, R>>> {
    type Output = <P as Running<St<Nil, F, Cons<C, R>>>>::Output;
}

Rust unifies Left<P1> from the trait with Left<P2> that we’re asking it to unify with. (The variables have the same letter, but they’re technically different so I’m naming them P1 and P2 here.) This works out fine; Rust unifies P1 with P2 and unification succeeds. Then, Rust unifies St<Nil, C, R1> with St<Nil, F, R2>. This succeeds; Nil is concrete, and Nil == Nil. The concrete type F is assigned to the variable C. And finally, the variables R1 and R2 are unified without complaints.

Now we have the substitution [P1 -> P2, C -> F, R1 -> R2] which is substituted into the body of the impl. We end up with this:

impl Running<St<Nil, F, R2>> for Left<P2>
    where P2: Running<St<Nil, F, Cons<F, R2>>> {
    type Output = <P2 as Running<St<Nil, F, Cons<F, R2>>>>::Output;
}

And so the “output type” of the “computation” is <P2 as Running<St<Nil, F, Cons<F, R2>>>>::Output.

Now that we’ve got that under our belts, let’s look at the handling for the Flip instruction in Running:

forall (P: ProgramTy, L: List, R: List) {
    [(Flip P), (St L F R)] => (# P (St L T R))
    [(Flip P), (St L T R)] => (# P (St L F R))
}

So this is fairly straightforward. The left and right lists aren’t modified at all. We recursively call Run on the program after the Flip instruction, and change F -> T and T -> F by pattern-matching.

forall (P: ProgramTy, Q: ProgramTy, L: List, R: List) {
    [(Loop P Q), (St L F R)] => (# Q (St L F R))
    [(Loop P Q), (St L T R)] => (# (Loop P Q) (# P (St L T R)))
}

And here’s the most complex instruction – Loop<P, Q>. We check the current bit by pattern-matching. In the case that it’s F, which means 0 in terms of the runtime representation, we recursively run the part of the program after the loop, hence skipping the body of the loop. In the case that the current bit is T, we make two recursive calls. The first produces a new state by running the body of the loop. Then, we run Loop<P, Q> again with the new state. This allows the program to branch off of the current state again.

And now we’re totally finished with all the complicated bits! The last instruction to handle is just Empty. All Empty does is return the current state unmodified, and not recurse:

forall (S: StateTy) {
    [Empty, S] => S
}

Relax! You’re finished with the type-level nastiness. Here’s a code listing showing the full expanded version of the Running trait and its impls:

Wrap-up: Testing and Conclusions

Along with the type-level implementation, I include two macros, sf! and sf_test!, which allow for testing of the runtime implementation against the type-level implementation. Here they are, in all their fairly simple glory:

// A Smallfuck state which is filled with `F` bits - a clean slate.
pub type Blank = St<Nil, F, Nil>;


// Convert nicely formatted Smallfuck into type-encoded Smallfuck.
macro_rules! sf {
    (< $($prog:tt)*) => { Left<sf!($($prog)*)> };
    (> $($prog:tt)*) => { Right<sf!($($prog)*)> };
    (* $($prog:tt)*) => { Flip<sf!($($prog)*)> };
    ([$($inside:tt)*] $($outside:tt)*) => { Loop<sf!($($inside)*), sf!($($outside)*)> };
    () => { Empty };
}


macro_rules! sf_test {
    ($($test_name:ident $prog:tt)*) => {
         $(
            #[test]
            fn $test_name() {
                let prog = <sf! $prog as ProgramTy>::reify();

                let typelevel_out = <Run<sf! $prog, Blank> as StateTy>::reify();
                let runtime_out = prog.run();

                println!("Program: {:?}", prog);
                println!("Type-level output: {:?}", typelevel_out);

                let offset = runtime_out.ptr.wrapping_sub(typelevel_out.loc as u16);

                for (i, b1) in typelevel_out.bits.into_iter().enumerate() {
                    let b2 = runtime_out.get_bit((i as u16).wrapping_add(offset));
                    println!("[{}] {} == {}",
                            i,
                            if b1 { "1" } else { "0" },
                            if b2 { "1" } else { "0" });
                    assert_eq!(b1, b2);
                }
            }
         )*
    }
}

I have to credit durka for fixing my sf! macro, which was originally near-useless. Thanks much!

Two tests are also included with the full source code of the runtime and type-level implementations:

sf_test! {
    back_and_forth {
        > * > * > * > * < [ * < ]
    }
    forth_and_back {
        < * < * < * < * > [ * > ] > > >
    }
}

The tests check only the bits set by the type-level implementation relative to the location of the pointer, but it’s enough for me to be certain that the implementations are correct. Smallfuck is so simple there’s almost no room for error; nevertheless, if anyone would like to contribute more tests, I would welcome any pull requests.

So, Rust’s type system is Turing-complete. What does this mean?

Honestly, it means pretty much nothing. Sure, the type system can get into infinite loops, but we already have a recursion limit in the type checker so that’s nearly irrelevant. Sure, we can write things like Smallfuck in the type system. Okay, that last one’s kinda cool.

In most cases where the typechecker hits the recursion limit, something’s wrong with your program and it won’t compile no matter what. Only if you’re really mucking with the type system – like, say, writing seriously large Smallfuck programs with it – then maybe you’ll hit the recursion limit.

If you’re pushing the limits and trying to do things like encode integers or other information as types in Rust – like typenum, peano, type-level-logic – then it’s still a bit interesting, because it means that if you screw up, then you could end up causing infinite loops in the typechecker. Since Peano arithmetic is undecidable, you have to have a Turing-complete type system if you really want to abuse the type system in such a way that you can even begin to reason about it.

For further reading on Turing-completeness, I suggest looking at the Glasgow Haskell Compiler’s manual, specifically about extensions to typeclasses such as -XUndecidableInstances. Wikipedia also has a lot of fairly extensive material on the subjects of computability theory and logics.

One last time: the full source code of this project is available here, on GitHub. https://github.com/sdleffler/tarpit-rs