RusTollens - 类型级别的布尔逻辑

一个小型且实验性的 Rust 库，它使用类型级别的布尔表示，并带有相应的连接词，以便在编译时进行逻辑的有趣操作。

type Tollens<P, Q> = Imp<And<Imp<P, Q>, Not<Q>>, Not<P>>;

fn what_is_reality<T: Truth>() {}
what_is_reality::<Or<True, Not<True>>>();

其背后的直觉如下

考虑 trait Negation

trait Negation {
    type Output;
}

注意缺少关联函数，它只有一个关联 类型。

以及 Negation 对类型 True 和 False 的实现

struct True;
struct False;

impl Negation for True {
    type Output = False
}

impl Negation for False {
    type Output = True
}

我们可以将 Negation 视为从类型到类型的部分函数，其中 Self 是输入，Output 是输出，每种输入类型的组合产生一个函数（impl）。伪代码如下

negation(True) = False
negation(False) = True

具有更多输入的函数对应于具有泛型参数的 trait，如下面定义的 Conjunction

trait Conjunction<L> {
    type Output;
}

此时我们需要四个 impl 来穷尽 True 和 False 的四种组合，例如

impl Conjunction<True> for False {
    // False AND True IS False
    type Output = False;
}

RusTollens 建立在上述思想之上，用于在类型级别计算简单的逻辑语句，在编译时静态地计算。

可能不是一个非常适用的库，但将不变量编码在类型级别，以便编译器可以代表我们验证它们，这个想法非常强大。因此，这个小型实验旨在提供一些思考的素材，并邀请读者探索并充分利用 Rust 的类型系统。