- 💬 写在前面：本章我们将继续讲解类型系统，定义我们设计的 F- 语言的类型、环境和类型规则。
目录
0x01 定义类型环境：𝚪 ∈ 𝑻𝒚𝑬𝒏𝒗 = 𝑽𝒂𝒓 → 𝑻
0x00 定义类型：𝝉 ∈ 𝑻𝒚𝑽𝒂𝒓 = 𝑺𝒕𝒓𝒊𝒏𝒈
我们可以使用推理规则来定义我们的 F- 语言中的类型集合 。
使用符号 来表示类型变量：
为了与程序变量区分开，我们将使用以 ' 符号开头的名称。
例如 bool, int, 'a, 'b, … ，例如 bool -> int, int -> (int -> bool), 'a -> int, …
0x01 定义类型环境：𝚪 ∈ 𝑻𝒚𝑬𝒏𝒗 = 𝑽𝒂𝒓 → 𝑻
在设计我们的 F- 语言的类型系统之前，让我们先定义一下类型环境 (Type Environment) ：
- 类型环境是从变量到类型的映射。例如：{ 𝑥 ↦ int, 𝑦 ↦ bool , 𝑧 ↦ 'a }
我们使用符号 来表示类型环境：
比较一下，在之前的语义定义中，环境是从变量到值的映射：
0x02 定义类型规则：𝚪 ⊢ 𝒆 : 𝑡
接下来，我们定义关系：
表达的意思是：在给定类型环境 ，表达式
的类型必须是
。
换句话说，如果 ，则表达式
的类型是
(并非充分必要条件) 。
比较一下，在语义定义中，我们写过 𝝆 ⊢ 𝒆 ⇓ 𝒗，意思是 "给定环境 𝝆，表达式 𝒆 被求值为值 𝒗"
对于 if-then-else 表达式，证明 Γ ⊢ if 𝑒1 then 𝑒2 else 𝑒3 ∶ 𝑡，𝑒2, 𝑒3 必须具有相同的类型 𝑡 。
例如，对于程序 = "if true then 1 else false"：
- 我们可以证明
，即
的执行结果是 1。
- 但我们无法证明
，因为类型规则不接受这种情况。
这个规则表明，对于 if-then-else 表达式来说，
分支 𝑒2 和 𝑒3 的类型必须一致，才能在类型环境 𝚪 下证明整个表达式的类型为 𝑡：
📌 [ 笔者 ] 王亦优
📃 [ 更新 ] 2024.6.14
❌ [ 勘误 ] /* 暂无 */
📜 [ 声明 ] 由于作者水平有限，本文有错误和不准确之处在所难免，
本人也很想知道这些错误，恳望读者批评指正！📜 参考资料 - R. Neapolitan, Foundations of Algorithms (5th ed.), Jones & Bartlett, 2015. - T. Cormen《算法导论》（第三版），麻省理工学院出版社，2009年。 - T. Roughgarden, Algorithms Illuminated, Part 1~3, Soundlikeyourself Publishing, 2018. - J. Kleinberg&E. Tardos, Algorithm Design, Addison Wesley, 2005. - R. Sedgewick&K. Wayne，《算法》（第四版），Addison-Wesley，2011 - S. Dasgupta，《算法》，McGraw-Hill教育出版社，2006。 - S. Baase&A. Van Gelder, Computer Algorithms: 设计与分析简介》，Addison Wesley，2000。 - E. Horowitz，《C语言中的数据结构基础》，计算机科学出版社，1993 - S. Skiena, The Algorithm Design Manual (2nd ed.), Springer, 2008. - A. Aho, J. Hopcroft, and J. Ullman, Design and Analysis of Algorithms, Addison-Wesley, 1974. - M. Weiss, Data Structure and Algorithm Analysis in C (2nd ed.), Pearson, 1997. - A. Levitin, Introduction to the Design and Analysis of Algorithms, Addison Wesley, 2003. - A. Aho, J. Hopcroft, and J. Ullman, Data Structures and Algorithms, Addison-Wesley, 1983. - E. Horowitz, S. Sahni and S. Rajasekaran, Computer Algorithms/C++, Computer Science Press, 1997. - R. Sedgewick, Algorithms in C: 第1-4部分（第三版），Addison-Wesley，1998 - R. Sedgewick，《C语言中的算法》。第5部分（第3版），Addison-Wesley，2002 |
![[14] CUDA_使用Opencv处理图像](https://img-blog.csdnimg.cn/direct/1b255ab0fd1b4af0aa97bc066df8f022.png)
