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