Set theory in Rust Programming Language

When I was reading Alex Zhang's Tao of Rust which is a comprehensive Rust book in Chinese, I found the Figure 3-5 on P70 in Chapter 3 improper.

Background

The section that attracted me is about how to describe trait bound in a mathematical way. In order to practice my skill of utilizing the Set Theory and have a clear picture of Rust's robust trait system, I decided to try it for myself.

Question

  • There are two arbitrary trait \(A\) and trait \(B\).
  • There is a type \(T\)

What can we infer from T: A + B.

Answer

Suppose we have three sets \(A, B, T\).

Inference A

The defination of \(A, B\) is \(\{method\ |\ method\ in\ the\ trait\}\). \[T=\{method\ |\ method\ that\ implemented\ by\ T\}\] Obviously, \[\begin{cases} \forall{}method_a\in{}A\\ \forall{}method_b\in{}B \end{cases}\] They satisfy \[\begin{cases} method_a\in{}T\\ method_b\in{}T \end{cases}\] So, \[T\supset{}(A\cup{}B)\]

Inference B

Suppose the \(TI\) is the acronym for \(TypeInstance\). If the defination of \(A, B\) is \(\{TI\ |\ TI\ that\ implemented\ the\ trait\}\). \[T=\{TI\ |\ TI\in{}type\ T\}\] If set \(C\) represents the \(TI\) s that implemented the trait \(A\) and trait \(B\). Obviously, \[C=A\cap{}B\] And if T: A + B is true, we can infer: \[T\subset{}C\] \[\therefore{}T\subset{}(A\cap{}B)\]

Conclusion

We can infer Inference A and Inference B from T: A + B

Reference

  1. 「第三章」`3.4.2 泛型约束` 数学角度描述 trait 中的概念混淆与逻辑错误 <https://github.com/ZhangHanDong/tao-of-rust-codes/issues/99>