原文链接: https://sdleffler.github.io/RustTypeSystemTuringComplete/
翻译：ChenYe
选题：aresbit
Rust类型系统图灵完备的证明
TL;DR: 本文使用 Rust 类型系统实现了 Smallfuck 的所用功能，证明了 Rust 的类型系统是图灵完备的。
译者前言：阅读本文需要了解 Rust 的 trait 机制，associated types ，以及泛型的相关知识。阅读时长约2h。
（注意：“fuck” 在本文中出现多次，但这个词在这里并不是污言秽语。）
不久前，有人在 Reddit Rust 子论坛上提出挑战：虽然每个人都喜欢说 Rust 的类型系统是图灵完备的，但实际上似乎还没有人给出确凿的证据。作为对那篇文章的回应，我以使用Rust 实现 Smallfuck（一种已知的图灵完备语言）的方式给出了一个证明，说明 Rust 的类型系统是图灵完备的。这篇文章将阐述 Smallfuck 的 Rust 实现的内部工作原理，以及这对 Rust 类型系统的意义。
那么什么是图灵完备性呢？图灵完备性是大多数编程语言的一个属性，它表明这些语言可以模拟通用图灵机。与之相关的概念是图灵等效。图灵等效语言可以模拟图灵机也可以被图灵机模拟——因此，如果你有任何两种图灵等效语言，则一定可以将使用一种语言编写的任何程序翻译成另一种语言所编写的程序。大多数图灵完备的系统也被认为是图灵等效的。（wiki）
关于图灵完备性，有几件重要的事情需要注意。假定你知道停机问题， 如果一个系统是图灵完备的，那么也意味着停机问题不可解决。也就是说，如果你有一种图灵完备的语言，它可以模拟任何通用图灵机，那么它必须能够无限循环。这就是为什么知道 Rust 的类型系统是否是图灵完备的很有用——这意味着，如果你能够将图灵完备的语言编码到 Rust 的类型系统中，那么检查 Rust 程序以确保它的类型是否正确的过程必须是不可判定的问题。即类型检查器必须能够进行无限循环。
我们如何证明 Rust 类型系统是图灵完备的？最直接的方法（实际上我不知道其他方法）是在其中实现一种已知的图灵完备语言。如果你可以用一种语言实现图灵完备的语言，那么你可以清楚地在其中模拟任何通用图灵机，也就说明这种语言是图灵完备的。
Smallfuck: 有啥用
那么，什么是 Smallfuck？ Smallfuck 是一种极简的编程语言，当内存限制被解除时，它就是图灵完备的。我选择将它在 Rust 类型系统中实现而不是其他图灵完备的语言，就是因为它很简单。
实际上 Smallfuck 非常接近图灵机本身。 根据 Smallfuck 的原始规范声明，它是运行在内存有限的机器上的。然而，如果我们解除这个限制并允许它访问理论上无限的内存数组，那么 Smallfuck 就变成了图灵完备的。所以在这里，我们考虑一种具有无限内存的 Smallfuck 的变体。 本文中 Smallfuck 机器由无限的内存磁带组成，该磁带由包含位的“单元”以及指向该单元的指针组成。
Pointer |
v
...000001000111000001000001111...Smallfuck 程序是由五个指令组成的字符串：
< | 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利用这几种指令就能够选择内存单元格并制作循环程序。这是一个简单的示例程序：
>*>*>*[*<]这是一个非常简单且完全没用的程序（大多数 Smallfuck 程序都没啥用，这要归因于它完全没有任何类型的 I/O），它只是将指针所指位置的后三位设置为 1，然后使用循环将它们全部置回 0，最后指针停在它开始时候的位置。下面我们来看一下这个过程：
首先，以下是初始状态：
Instruction pointer
| Memory pointer
v v
>*>*>*[*<] | ...0...第一条指令将指针向右移动。所有单元格默认为 0：
v v
>*>*>*[*<] | ...00...下一条指令是“翻转当前位”指令，因此我们将指针处的位从 0 翻转到 1。
v v
>*>*>*[*<] | ...01...这种情况发生了 3 次。我们跳过重复来到循环的开头：
v v
>*>*>*[*<] | ...0111...现在我们处于循环的开始。 [ 指令是说，“如果当前位为零，则跳转到匹配的 ]；否则，转到下一条指令。” 当前指针所指是 1，所以我们转到下一条指令。
v v
>*>*>*[*<] | ...0111...这会将当前位翻转回零；然后，我们将内存指针移回一个位置。
v v
>*>*>*[*<] | ...0110...现在我们来到循环结束符]，无条件跳回到循环开始处。
v v
>*>*>*[*<] | ...0110...现在我们再次分支。当前单元格为 0 吗？显然不为 0，然后我们继续：
v v
>*>*>*[*<] | ...0110...
v v
>*>*>*[*<] | ...0100...
v v
>*>*>*[*<] | ...0100...
v v
>*>*>*[*<] | ...0100...在最后一次循环之后，我们结束了：
v v
>*>*>*[*<] | ...0000...这正是我们开始的地方：所有单元格归零，并且指针位于其起始位置。
Smallfuck 在 Rust 中的 Runtime
那么在 Rust 中这个简单的实现会是什么样子呢？首先我要介绍我实现的 Smallfuck Runtime 的实现，以验证 Rust type-level 和 Smallfuck 运行时实现是否一致。我们会将 Smallfuck 程序存储为枚举类型定义的 AST 节点，如下形式：
enum Program {
Empty,
Left(Box<Program>),
Right(Box<Program>),
Flip(Box<Program>),
Loop(Box<(Program, Program)>),
}这种表示方法对于字符串形式的 Smallfuck 程序并非十分精确，但它更容易理解。我们还需要一个类型来表示正在运行的 Smallfuck 程序的状态：
struct State {
ptr: u16,
bits: [u8; (std::u16::MAX as usize + 1) / 8],
}尽管要实现图灵完备，我们在技术上需要无限长的磁带，但我们的运行时实现仅仅是为了检查 Rust 类型系统的语义正确性。所以说，这里我们使用一个有限长的磁带作为近似就可以了。通过使用长度为(std::u16::MAX as usize + 1) / 8的bits，我们确保每个u16指针可以指向的范围内都是可用的。现在我们来定义实现 Smallfuck 程序解释器时需要用到的一些操作：
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);
}
}这是一些标准的位操作。我们将 8 位存储到我们的位数组中的一个单元格中，这样一来要找出给定的指针指向哪个单元格：将指针向右移位三位，然后使用指针的低三位作为单元格内部的索引，就找到了目标 bit 位。
ptr = 0b1100011010011001
Index into the bytes of `bits` --> 1100011010011 \ 001 <-- Which bit in the byte具体来说，这个寻址操作就如是上面的函数get_bit所示，将指针at>>3作为单元格寻址，通过bits[(at >> 3) as usize]取出单元格，然后使用0x7即0b111作为掩码取at的低三位，作为单元格内的偏移量，将0x1左移偏移量，再按位与上单元格就得到了目标bit是1还是0，对应函数返回true和false。同样的flip_current_bit也按相同的方式取出目标bit位，然后异或上0x1，将原bit位取反。
现在我们有了这些原语，让我们继续实现我们的解释器。我们将通过递归调用一个在枚举类型 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!(),
}
}
}Empty 程序不修改任何状态，因此其实现非常简单：
Empty => {},Left 和 Right 只是将指针加/减一。由于我们在简单实现中选择使用有限的内存磁带，因此我们使用 wrapping_add 和 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 非常简单，因为我们已经写了方便的 flip_current_bit 函数：
Flip(ref next) => {
state.flip_current_bit();
next.big_step(state);
},最后是循环。我们需要检查当前位。如果是 1，那么我们执行循环体，然后以更新的状态再次执行循环指令。如果为 0，我们继续循环体后的下一条指令：
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);
}
},注意，我们必须对 body_and_next 进行双重解引用，因为我们是将一个元组(Program, Program)装入Box<>中（见 Program 的定义）。我们通过 ref 来避免将 body 和 next 的所有权从 Box 中移走。最终我们为枚举类型 Program 完成的 .big_step() 函数如下所示：
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);
}
},
}
}
}我们不会为State实现任何类型的调试打印，因为我们不需要。当使用我们的实现 Smallfuck 运行时解释器来检查 Rust type-level 解释器时，我们将通过检查 Rust type-level 解释器的输出，和 Smallfuck 运行时解释器输出，的一致性来完成检验。现在，我们终于可以开始做些有趣的事情了！
Type-Level Smallfuck in Rust
Rust 有一个称为 traits 的特性。 Traits 是一种进行编译时静态分派的方法，也可以用于执行运行时分派（尽管在实践中很少见），这里假设读者知道 Rust 中有这些特征并且已经大量使用过。为了实现 Smallfuck，我们将依赖于被称为 associated types 的特性。
这里 associated types 可参考：关联类型 。
Trait resolution and unification
在 Rust 中，为了调用 trait methods 或解析 associated types ，编译器必须经过一个称为 trait resolution 的过程。为了解析一个 trait ，编译器必须寻找一个与所涉及的 types 相对应的 impl。Unification 是求解 types 之间等式的过程。如果没有解，我们就说 unification 失败了。举个例子：
trait Foo<B> {
type Associated;
}
impl<B> Foo<B> for u16 {
type Associated = bool;
}
impl Foo<u64> for u8 {
type Associated = String;
}为了解析对一个 associated type （e.g. <F as Foo<T>>::Associated）的引用，Rust 编译器必须找到一个 impl ，这个实现能正确匹配 F 和 T 。假设我们有F == u16和T == u64。如果编译器尝试第二个 impl Foo<u64> for u8，它会发现 F 不匹配 u8，这个实现是不可行的。如果它尝试第一个实现，就得到 F == u16，此时 F 匹配正确。现在我们必须匹配 T == B。这里就是最 magic 的地方。
Rust 编译器将尝试 unify T 和 B 。由于 B 是一个泛型——不是具体类型，它的值可以是 String 或 u64 等等可以被随意赋予。所以现在 B 被 u64 替换，我们有了一个 Foo<u64> for u16 的 impl，这是一个可行的解析。Unification 是一个相当简单的过程：它接受一个可能有泛型的类型，每次它遇到一个尚未分配的泛型，且这个泛型匹配任何其他的类型，就将这个泛型分配给这个类型（即使其他类型也是泛型）。然后，任何时候在 unifies 同一个类型时遇到该泛型，它被其分配的值替换，相反，unification 尝试将分配的类型与另一个类型统一起来。
Unification 操作可以理解为一组“代换”——泛型到类型的映射，这样当你采用类型时，你就在试图 unify 并替换所有出现的泛型，你最终会得到两个相同的类型。下面是一个独立的 unification 示例，尝试使用Foo<Baz, Y> unify Foo<X, Bar<u16, Z> （X，Z 为泛型，Foo，Baz，Bar 为具体类型）：
Foo<X, Bar<u16, Z>> == Foo<Baz, Y>首先，我们检查类型的头部——我们得到 Foo vs. Foo ，并没有失败。如果我们有，比如说，Foo == Bar 那么 unification 就直接失败了。接下来，我们将其分解为两个子问题。我们知道 Foo<A, B> == Foo<C, D> 当且仅当 A == C 和 B == D：
X == Baz, Bar<u16, Z> == Y我们现在已经解决了一个变量——X，它有一个明确定义的值：Baz 。可以将这个泛型和类型之间的关系添加到我们的代换表中，[X -> Baz]。然后，我们将该代换表应用于第二项 Bar<u16, Z> == Y。因为代换表里没有出现 X，所以什么也没有发生。然后，我们得到了 Y 的替换方案。此时，代换表：[X -> Baz, Y -> Bar<u16, Z>]。让我们观察当我们将其应用于我们想要检查的原始方程时会发生什么：
Foo<X, Bar<u16, Z>> == Foo<Baz, Y> [X -> Baz, Y -> Bar<u16, Z>]转换为：
Foo<Baz, Bar<u16, Z>> == Foo<Baz, Bar<u16, Z>>这个等式方程显然是成立的。这两个变量现在相等了！那么 unification 失败的例子是什么样的？咱们试试吧：
Foo<Bar, X> == Foo<X, Baz>这分解为两个等式：
Bar == X, X == Baz所以我们求解第一个方程，得到代换表 [X -> Bar]。应用代换表到 x == Baz 产生了 Bar == Baz 这显然是错误的，unification 失败了——没有可行的解。
Unification 是一个非常有用的过程，实际上存在一种编程语言 Prolog ，它通过逻辑表达式描述程序，其程序的执行过程就是表达式的 unification 的过程。这听起来有点让人摸不着头脑。实际上，如果有一种基于 Unification 的图灵完备语言 Prolog，那么 Rust 的 trait 解析（通过尝试unify trait impl 直到找到可行的实现）似乎也应该是图灵完备的.
Computing with traits
现在我们已经完成了样板文件，让我们看看我们如何在 Rust 中实际编写实现Smallfuck。我们将使用我几个月前编写的一个名为 type_operators! 的宏，它将 DSL 编译成 Rust struct definitions、trait defination 和 trait impls 的集合。接下来我们首先要来看看type_operators!的实现。
我们将从简单开始，我们如何在 Rust 类型中表示 Smallfuck 状态的位？
type_operators! {
[ZZ, ZZZ, ZZZZ, ZZZZZ, ZZZZZZ]
concrete Bit => bool {
F => false,
T => true,
}
}这里有几点需要注意。第一个就是这个有点奇怪的 list，[ZZ, ZZZ, ZZZZ, ZZZZZ, ZZZZZZ] 。这很难解释，但它与 Rust 宏无法创建唯一类型名称有关。因此，你必须通过提供自己的 list 的方式来解决这个问题。你可以暂时忽略这一点，因为它与实际实现无关。但是， concrete Bit 是我们必须要搞清楚的！
type_operators! 接受了两种类型级别的伪数据类型定义：data 和 concrete 。这两个宏关键字的区别在于 type_operators! 生成 traits 以确保你不会与这些 type-level 的数据类型不匹配。上面的宏代码将会编译为以下定义：
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 }
}希望你能看明白发生了什么。T 和 F 成了单个的实现了 Bit 的 structs 。Bit 为它们提供了一个 reify() 函数，可让你将类型 T 和 F 转换为相应的布尔表示。所以你可以写 <T as Bit>::reify() 它将返回 true 。这很有用，因为只要你有一个 Bit 类型的变量 B: Bit，你就可以使用 B::reify() 返回其对应的 bool 值。我使用它来将 Smallfuck 解释器的输出转换为可以检查其运行时实现的值。
希望我表达的足够清楚！让我们看看另一个使用 concrete 的定义：
concrete List => BitVec {
Nil => BitVec::new(),
Cons(B: Bit, L: List = Nil) => { let mut tail = L; tail.push(B); tail },
}这里有点复杂了。让我们慢慢讲一讲。
这是一个 type-level cons-list 。我们从代码中首先可以看到一对结构类型，Nil 和 Cons ，它们将被宏解析为：
pub struct Nil;
pub struct Cons<B: Bit, L: List = Nil>(PhantomData<(B, L)>);所以，现在我们得到了 bits 和 bits 的 lists 。我们可以构造一个列表[T, F, F]作为Cons<T, Cons<F, Cons<F, Nil>>>。除此之外，宏还使我们获得了一些 traits：
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
}
}所以要注意的一件事是，我们写的调用宏的代码中：
Cons(B: Bit, L: List = Nil) => { let mut tail = L; tail.push(B); tail }它会产生一种语法糖，其中 L 和 B 被自动具体化为具体类型，然后绑定到这些类型中。这是为了绕过 macro hygiene 的一些限制，并允许用户实际使用这些值。
所以希望现在你已经弄清楚了，让我们看看我们实现 Smallfuck 将使用的最后两个使用 concrete 的定义：
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,
}
},
}希望你现在已经弄清楚了所有的模式。以下是一个完整的清单，展示了所有这些使用 type_operators! 宏的定义是如何编译成 Rust structs， traits， 和 impls ：
// `Bit` trait and `T` and `F` types.
pub trait Bit {
fn reify() -> bool;
}
pub struct F;
pub struct T;
impl Bit for F {
fn reify() -> bool {
false
}
}
impl Bit for T {
fn reify() -> bool {
true
}
}
// `List` trait and `Nil` and `Cons<H, T>` types.
pub trait List {
fn reify() -> BitVec;
}
pub struct Nil;
pub struct Cons<B: Bit, L: List = Nil>(PhantomData<B>, PhantomData<L>);
impl List for Nil {
fn reify() -> BitVec {
BitVec::new()
}
}
impl<B: Bit, L: List> List for Cons<B, L> {
#[allow(non_snake_case)]
fn reify() -> BitVec {
let B = <B>::reify();
let L = <L>::reify();
{
let mut tail = L;
tail.push(B);
tail
}
}
}
// `ProgramTy` trait and `Empty`, `Left<P>`, `Right<P>`, `Flip<P>`, and `Loop<P, Q>` types.
pub trait ProgramTy {
fn reify() -> Program;
}
pub struct Empty;
pub struct Left<P: ProgramTy = Empty>(PhantomData<P>);
pub struct Right<P: ProgramTy = Empty>(PhantomData<P>);
pub struct Flip<P: ProgramTy = Empty>(PhantomData<P>);
pub struct Loop<P: ProgramTy = Empty, Q: ProgramTy = Empty>(PhantomData<P>, PhantomData<Q>);
impl ProgramTy for Empty {
fn reify() -> Program {
Program::Empty
}
}
impl<P: ProgramTy> ProgramTy for Left<P> {
#[allow(non_snake_case)]
fn reify() -> Program {
let P = <P>::reify();
Program::Left(Box::new(P))
}
}
impl<P: ProgramTy> ProgramTy for Right<P> {
#[allow(non_snake_case)]
fn reify() -> Program {
let P = <P>::reify();
Program::Right(Box::new(P))
}
}
impl<P: ProgramTy> ProgramTy for Flip<P> {
#[allow(non_snake_case)]
fn reify() -> Program {
let P = <P>::reify();
Program::Flip(Box::new(P))
}
}
impl<P: ProgramTy, Q: ProgramTy> ProgramTy for Loop<P, Q> {
#[allow(non_snake_case)]
fn reify() -> Program {
let P = <P>::reify();
let Q = <Q>::reify();
Program::Loop(Box::new((P, Q)))
}
}
// `StateTy` trait and `St` type.
pub trait StateTy {
fn reify() -> StateTyOut;
}
pub struct St<L: List, C: Bit, R: List>(PhantomData<L>, PhantomData<C>, PhantomData<R>);
impl<L: List, C: Bit, R: List> StateTy for St<L, C, R> {
#[allow(non_snake_case)]
fn reify() -> StateTyOut {
let L = <L>::reify();
let C = <C>::reify();
let R = <R>::reify();
{
let mut bits = L;
let loc = bits.len();
bits.push(C);
bits.extend(R.into_iter().rev());
StateTyOut {
loc: loc,
bits: bits,
}
}
}
}from: https://gist.github.com/sdleffler/46700a8add454bc23cdb399a766cb273#file-rust-smallfuck-concretes-rs
从上面的代码可见 ProgramTy 相当简单，希望你现在明白为什么我选择将 Smallfuck 程序的运行时编码为 AST 的形式—— 为了尽可能清晰地反映 Rust type-level encoding。 StateTy trait 下的 St 类型是一个 zipper list ，同时表示 Smallfuck 解释器的指针位置和内存。 L 和 R 列表表示 C 两侧的内存，C 是指针下的当前位。
现在我们可以看看最有趣的部分——Smallfuck 解释器的实际实现。它由一个 trait 和十几个 impl 组成。以下是 type_operators! 宏中的代码：
(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
}
}这些使用宏的代码将编译成一大堆东西。首先来说有一个 trait ，如下代码所示。
这就是奇怪的 gensym list 发挥作用的地方。由于 gensyms 只在这里使用，它们不会与用户编写的任何内容发生冲突，因为这里没有写入任何涉及泛型的内容。由于写 ZZ, ZZZ 等是一件痛苦的事情，这里我选择忽略，不过多叙述我实际放到 gensym list 中的东西，只是简单的把它写好就得了。
上面一段并不重要，是原作者的自言自语，如果需要可以自行了解 Rust 的宏生成系统.
pub trait Running<S: StateTy>: ProgramTy {
type Output: StateTy;
}
pub type Run<P: ProgramTy, S: StateTy> = <P as Running<S>>::Output;(Run) Running(ProgramTy, StateTy): StateTy 成了一个 type-level 函数，输入参数是实现了 ProgramTy 和 StateTy 的两种 trait 的类型，输出是实现了 StateTy trait 的类型。
现在来看看里面的东西。让我们先看一个简单的定义：
forall (P: ProgramTy, C: Bit, R: List) {
[(Left P), (St Nil C R)] => (# P (St Nil F (Cons C R)))
}它编译为一个 trait impl ，如下所示：
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;
}(# P (St Nil F (Cons C R))) 的意思是：“递归地‘调用’带有参数 P (St Nil F (Cons C R)) 的 type-level 函数。” type_operators! 使用 lisp-like DSL 来简化解析； 写作 (A B C) ，编译为类型： A<B, C> 。 ‘# function’ 在 type_operators! 中是特殊的语法，因为必须追踪 ‘#’ 的使用情况，具体来说：每当调用 ‘#’ 时，必须在 where 子句中添加一个约束。你可以通过上面的示例看到这种用宏生成代码的动作是如何进行的。
现在类型级函数定义的语义已经明确了，我们来看看 Smallfuck 是怎么定义的。我们有四种不同的定义来处理 Left 和 Right指令：
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))
}第一个定义了当指针向左移动时会发生什么，但我们的拉链列表（zipper list）中左侧的 cons-list 是空的。我们必须创建一个新的 F bit（表示 0），并将当前位移动到右侧的 cons-list 中。左侧的 cons-list 保持为 Nil。
这里的第二个定义同上，现在是指针必须向右移动而右侧的 cons-list 为 Nil 的情况。
第三和第四个定义分别处理指针向左、右移动，且左、右的 cons-list 分别为 Cons<N, L> 和 Cons<N, R> 的情况。在这种情况下，我们可以从 cons-list 中弹出一个值并将其移动到当前位；然后将当前位压入另一个 cons-list 。下面来形象的说明这个四个过程：
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...]那么 Rust 究竟是如何“执行”这些向左向右动作的呢？假设当前程序为 Left<P> 当前状态是 St<Nil, F, R>。当我们将它们放入 Run<P, S> type synonym，使其成为 Run<Left<P>, St<Nil, F, R>> 时，我们最终得到 <Left<P> as Running<St<Nil, F, R>>>::Output 。这会使得 Rust 尝试搜索一个 impl 来做 unification 。
我们之前说过，由于 Rust 编写 trait 和 impl 的规则，对于任何给定的类型，Rust 尝试为其寻找 impl 最多只能有一个有效的 impl。 Rust 找到了我们手写的宏编译后会生成的 impl ：
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 将 trait 中的 Left<P1> （即宏代码中的 P）与我们要求它 unify 的 Left<P2> 统一起来。 （为 P1 和 P2 是不同的） Rust 将 P1 与 P2 统一起来，统一成功。然后，Rust 将 St<Nil, C, R1> 与 St<Nil, F, R2> 统一起来。这也可以成功； Nil 是具体的类型，Nil == Nil ，这没问题也可以统一。将具体类型 F 分配给泛型 C。最后，泛型 R1 和 R2 统一起来，顺利结束 unification。
现在我们有了代换表 [P1 -> P2, C -> F, R1 -> R2] ，它被替换到上述 trait impl 的主体中。我们最终得到了这个：
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;
}所以宏编译生成后的 “output type” 是 <P2 as Running<St<Nil, F, Cons<F, R2>>>>::Output 。
现在我们已经掌握了宏的运作原理，让我们看看 Running 中 Flip 指令的处理：
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))
}实际上这部分这相当简单。左右列表根本没有修改。我们在 Flip 指令之后对程序递归调用 Run，并通过模式匹配改变 F -> T 和 T -> F ，结束。
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)))
}循环指令 Loop<P, Q> 是最复杂的指令。我们通过模式匹配检查当前位。如果它是 F 即 0 ，则在运行时的表达就是：我们递归地运行循环之后的程序部分，也就是跳过循环体。如果它是 T 即 1 ，则在运行时的表达就是：我们进行两次递归调用。第一个通过运行循环体产生一个新状态。然后，我们再次使用新状态运行 Loop<P, Q> 。
现在我们已经完成了所有复杂的部分！最后要处理的指令只是 Empty。 Empty 所做的只是返回未修改的当前状态，而不是递归：
forall (S: StateTy) {
[Empty, S] => S
}现在，你已经完成了 type-level 实现 Smallfuck 运行时的所有困难工作。以下是代码，展示了 Running trait 及其 impls 的完整扩展版本：
pub trait Running<B: StateTy>: ProgramTy {
type Output: StateTy;
}
pub type Run<A: ProgramTy, B: StateTy> = <A as Running<B>>::Output;
// [(Left P), (St Nil C R)] => (# P (St Nil F (Cons C R)))
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;
}
// [(Right P), (St L C Nil)] => (# P (St (Cons C L) F Nil))
impl<P: ProgramTy, L: List, C: Bit> Running<St<L, C, Nil>> for Right<P>
where P: Running<St<Cons<C, L>, F, Nil>>
{
type Output = <P as Running<St<Cons<C, L>, F, Nil>>>::Output;
}
// [(Left P), (St (Cons N L) C R)] => (# P (St L N (Cons C R)))
impl<P: ProgramTy, L: List, C: Bit, N: Bit, R: List> Running<St<Cons<N, L>, C, R>> for Left<P>
where P: Running<St<L, N, Cons<C, R>>>
{
type Output = <P as Running<St<L, N, Cons<C, R>>>>::Output;
}
// [(Right P), (St L C (Cons N R))] => (# P (St (Cons C L) N R))
impl<P: ProgramTy, L: List, C: Bit, N: Bit, R: List> Running<St<L, C, Cons<N, R>>> for Right<P>
where P: Running<St<Cons<C, L>, N, R>>
{
type Output = <P as Running<St<Cons<C, L>, N, R>>>::Output;
}
// [(Flip P), (St L F R)] => (# P (St L T R))
impl<P: ProgramTy, L: List, R: List> Running<St<L, F, R>> for Flip<P>
where P: Running<St<L, T, R>>
{
type Output = <P as Running<St<L, T, R>>>::Output;
}
// [(Flip P), (St L T R)] => (# P (St L F R))
impl<P: ProgramTy, L: List, R: List> Running<St<L, T, R>> for Flip<P>
where P: Running<St<L, F, R>>
{
type Output = <P as Running<St<L, F, R>>>::Output;
}
// [(Loop P Q), (St L F R)] => (# Q (St L F R))
impl<P: ProgramTy, Q: ProgramTy, L: List, R: List> Running<St<L, F, R>> for Loop<P, Q>
where Q: Running<St<L, F, R>>
{
type Output = <Q as Running<St<L, F, R>>>::Output;
}
// [(Loop P Q), (St L T R)] => (# (Loop P Q) (# P (St L T R)))
impl<P: ProgramTy, Q: ProgramTy, L: List, R: List> Running<St<L, T, R>> for Loop<P, Q>
where Loop<P, Q>: Running<<P as Running<St<L, T, R>>>::Output>,
P: Running<St<L, T, R>>
{
type Output = <Loop<P, Q> as Running<<P as Running<St<L, T, R>>>::Output>>::Output;
}
// [Empty, S] => S
impl<S: StateTy> Running<S> for Empty {
type Output = S;
}测试和结论
除了 type-level 的实现，还实现了两个宏，sf! 和 sf_test! ，用于测试我们的实现：
// 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);
}
}
)*
}
}我必须感谢 durka 修复了我的 sf! 宏，原本的几乎不能用。非常感谢！
完整源代码还包括两个测试：
sf_test! {
back_and_forth {
> * > * > * > * < [ * < ]
}
forth_and_back {
< * < * < * < * > [ * > ] > > >
}
}测试只检查了type-level 实现相对于指针位置设置的比特位，但足以让我确定我的实现是正确的。 Smallfuck 非常简单，几乎没有出错的余地；尽管如此，如果有人想贡献更多的测试用例，我很欢迎 pr 请求。
所以，Rust 的类型系统是图灵完备的。这是什么意思？
老实说，这几乎没有任何意义。类型系统确实可以进入无限循环，但我们已经在类型检查器中有递归限制，所以这个证明几乎没啥用。当然，我们可以在类型系统中编写 Smallfuck 之类的东西。好吧，最后这个还有一点点炫。
在类型检查器达到递归限制的大多数情况下，你的程序会无法编译。只有当你真的很向嘲讽 Rust 的类型系统时，那你可以尝试用它编写非常大的 Smallfuck 程序，此时，你可能会达到递归限制。
如果你正在挑战极限并尝试将整数或其他信息编码为 Rust 中的类型——比如 typenum、peano、type-level-logic——那么本文的证明会有点用，因为基于本文的证明，如果你搞砸了，那么你最终可能会在类型检查器中产生无限循环。
由于 Peano 问题是不可判定的，如果你真的想以一种甚至可以做逻辑推理的方式滥用一个类型系统，那你就必须有一个图灵完备的类型系统。
为了进一步了解图灵完备性，我建议查看 Glasgow Haskell Compiler 的手册，特别是关于 typeclasses 的扩展，例如 - XUndecidableInstances 。维基百科也有很多关于可计算性理论和逻辑科学的学习资料。
最后，该项目的完整源代码可在此处获取，位于 GitHub 上。
https://github.com/sdleffler/tarpit-rs
原文写于 March 7, 2017，翻译于 May 4, 2022