#+BEGIN_COMMENT
.. title: Set theory in Rust Programming Language
.. slug: set-theory-in-rust-programming-language
.. date: 2019-06-11 10:30:10 UTC+08:00
.. tags: Rust, Set Theory, Learning Rust, Tao of Rust
.. category: Program
.. link:
.. description: 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.
.. type: text
.. has_math: true
#+END_COMMENT
#+BEGIN_QUOTE
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.
#+END_QUOTE
{{{TEASER_END}}}
* 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 [[infA][Inference A]] and [[infB][Inference B]] from ~T: A + B~
* Reference
1. /「第三章」`3.4.2 泛型约束` 数学角度描述 trait 中的概念混淆与逻辑错误/ <[[https://github.com/ZhangHanDong/tao-of-rust-codes/issues/99][https://github.com/ZhangHanDong/tao-of-rust-codes/issues/99]]>