Junglefowl

一次证明，残忍地摧毁 Rust 的类型系统。

Junglefowl 在 Rust 类型上运行 Peano 算术，并在编译时进行验证。

为什么？

这样我们就可以做理论上的困难事情，比如这些 const 泛型切片

use junglefowl::*;

// Accept only `u8` arrays with exactly 3 elements:
fn picky<T: Nest<Element = u8, Length = peano!(3)>>(_: &T) {}

// Create an array with 5 elements:
let n12345 = nest![1, 2, 3, 4, 5];

// Split it after its second element without changing anything in memory:
let (left, right) = split!(n12345, 2);

// And we can prove that the second segment will have exactly two elements:
picky(&right);
// picky(&left); // won't compile!

// And know exactly what its elements are:
assert_eq!(nest![3, 4, 5], right);

如何？

这是我们的 Peano 编码

0 <-->                ()
1 <-->           ((), ())
2 <-->      ((), ((), ()))
3 <--> ((), ((), ((), ())))

注意，由于巧妙地滥用 Rust 的语法，这些既是类型也是值。

接下来，有一个宏，你可以忘记你刚才读到的

peano!(0);
 --> ()
peano!(42);
 --> ((), ((), ((), ((), ((), ((), ((), ((), ((), ...)))))))))

注意，这个宏扩展为 类型，所以你会像这样使用它

let x: peano!(42) = todo!();

而不是这样

let x = peano!(42); // bad!

接下来，还有很多其他东西，但为了不解释所有这些，请看编译过程

static_assert_eq!(peano!(39), sub!(peano!(42), peano!(3)));

扩展为

enum False {} // uninstantiable type

//      this part vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv evaluates to zero when the two sides are equal
const _: [False; (peano!(39) != sub!(peano!(42), peano!(3))) as usize] = [];
// ... which makes the list length zero, which matches the right-hand side (and couldn't be nonzero since its members are uninstantiable)
// learned the list length trick from the `static_assertions` crate, so all credit there!

扩展上面的有趣部分（并且反转，以便将 != 转换为 ==）

peano!(39) == <         peano!(42)          as peano::Sub<     peano!(3)     >>::Difference;
peano!(39) == <((), ((), ((), peano!(39)))) as peano::Sub<((), ((), ((), ())))>::Difference;

这是 peano::Sub 的定义，对于这个包中的大多数操作来说相当典型

pub trait Sub<R: peano::N>: peano::N { type Difference: peano::N; } // sealed trait
impl<T: peano::N> Sub<()> for T { type Difference = Self; } // subtracting zero is our super-simple base case
impl<L: peano::N + Sub<R>, R: peano::N> Sub<((), R)> for ((), L) { type Difference = sub!(L, R); } // otherwise, reduce the problem until it's dividing by zero

开始化简！

peano!(39) == <((), ((), ((), peano!(39)))) as peano::Sub<((), ((), ((), ())))>::Difference;
peano!(39) == <     ((), ((), peano!(39)))  as peano::Sub<     ((), ((), ())) >::Difference;
peano!(39) == <          ((), peano!(39))   as peano::Sub<          ((), ())  >::Difference;
peano!(39) == <               peano!(39)    as peano::Sub<               ()   >::Difference;
peano!(39) ==                 peano!(39)                                                   ;

就这样！

这个名字的由来是什么？

一个著名的定理证明器是以法语中公鸡（coq）的名字命名的，所以我谷歌了“公鸡”并惊讶地发现它们属于 junglefowl 这一物种。这个名字听起来很酷。