这篇文章是关于子结构类型理论如何应用于编程语言设计的解释。

• 编程语言设计中的隐喻：编程语言设计师在思考如何呈现语言时，应发明隐喻来帮助普通程序员理解，如“所有权”这一术语。

• 类型系统与正确性属性：

  • 类型系统是形式方法中已被简化的部分，用于验证程序行为的方面，分为安全性属性（保证“坏事不发生”）和活性属性（保证“好事发生”），通常认为类型系统维护某些安全性属性，但由于语言的表达能力，活性属性通常有局限性。
  • 所有权是一种扩展语言类型系统的方法，用于建立关于程序安全性和活性属性的额外保证，特别是关于给定值被使用的次数。

• 子结构类型是什么：

  • 在数学逻辑中，有“结构规则”，如弱化和收缩，不包含这些规则的逻辑被称为子结构类型，其值在使用次数上受到限制。
  • Rust 中默认类型不具有收缩律，大多为仿射类型，只能使用一次或零次，通过“移动”或“丢弃”来处理；也支持可多次使用的普通类型，当前通过实现Copy或Clone trait 来实现。

• 线性类型和会话类型：

  • Rust 目前没有不能弱化的类型，但线性类型很有价值，以会话类型为例，它通过在类型系统中编码并发执行过程的协议来确保操作的合法性。
  • 线性会话类型通过防止丢弃会话类型、使用解构和隐私限制来实现活性保证，但 Rust 实现仿射类型时存在缺陷，如 E0509 错误，应结合解构和隐私来解决。

• 共享所有权：

  • 有时需要允许拥有的值被别名，这通过“共享所有权”来实现，要注意同步和循环问题，Rust 选择了允许不进行循环打破的引用计数指针，也可以通过引用和可变引用来实现。
• 结论：作者希望通过这篇文章让更多人了解所有权和子结构类型，认为新编程语言应包含子结构类型，Rust 也应改变所有权规则，如添加线性类型、解除 E0509 错误等。