- 💭 写在前面：本章我们将进入类型系统的讲解，回顾一下之前我们整理的 F- 语言，然后介绍一下静态分析和静态类型系统。讨论程序员该如何处理一些 bug，有没有完美的静态分析器。
目录
0x00 回顾：F- 语言
0x01 静态分析（Static Analysis）
0x02 静态类型系统（Static Type System）
0x03 什么是类型？
0x00 回顾：F- 语言
我们之前定义了简化版 F# 的语法和语义，并将其命名为 F-。
这是没有匿名 / 递归函数的版本：
我们还实现了一个解释器，根据语义定义运行程序，程序的执行意味着对F中的表达式进行求值。
floyd:~/Lab3$ cd FMinus/
floyd:~/Lab3/FMinus$ ls
FMinus.fsproj src testcase
floyd:~/Lab3/FMinus$ ls src
AST.fs FMinus.fs Lexer.fsl Main.fs Parser.fsy Types.fs
（let rec evalExp (exp: Exp) (env: Env) : Val =）请记住，某些在语法上有效的 F 程序未定义其语义。直观地说，这种情况相当于程序错误（漏洞），例如：类型不匹配、使用未绑定变量、除零错误，到目前为止，这些错误是在运行时捕获的（通过引发异常）
在现实世界中的编程语言中，还可能存在各种其他类型的错误（bug），例如：缓冲区溢出、悬空指针、未初始化数据的使用，等等。
有时，即使程序的语义定义是明确的，也可能存在问题，例如：逻辑错误、内存泄漏，等等。
0x01 静态分析（Static Analysis）
每个人都知道漏洞普遍存在且很重要，程序员无法避免犯错，我们应该如何处理这些漏洞？
开发一种能够在运行前检测漏洞的自动化技术怎么样？
- 自动化：由程序分析，而非人工
- 运行前：防止其在实际运行中引发严重问题
这种技术（或用于此的工具/程序）被称为静态分析（静态分析器），请记住，在编程语言中，静态表示 "在运行前决定"。
但遗憾的是，完美的静态分析器是不存在的，编写一个完美的程序分析算法被证明是不可能的（不可判定问题），参见自动机理论中的停机问题。
这里，完美是指健全性和完备性：
- 健全性：有错误的程序总是被拒绝 / 从不遗漏错误 / 如果程序通过检查，保证没有错误
- 完备性：没有错误的程序总是被接受 / 从不拒绝安全的程序 / 如果被拒绝，必定有错误
我们必须在健全性和完备性之间做出取舍，有时，我们甚至两者都要放弃。
尽管如此，这样的静态分析器（带有近似性）仍然是有用的。
0x02 静态类型系统（Static Type System）
静态类型系统是最原始和最流行的静态分析器形式之一，其目标是在运行前自动检测类型错误，通常作为编译器或解释器的一部分配备。
我们应该选择哪一方面：健全性还是完备性？ F# 采用的是健全（但不完备）的类型系统，本专栏我们也将讨论 F- 的健全类型系统。
0x03 什么是类型？
类型是一组值，或者可以将其视为值的抽象。
bool： { 真, 假 }
int： { … , -2, -1, 0, 1, 2, … }
int -> int：接受一个整数并返回一个整数的函数集合：
let incr : int -> int = fun x -> x + 1 'a -> 'a：接受任意类型 'a 并返回相同类型的函数集合：
let identity : 'a -> 'a = fun x -> x
📌 [ 笔者 ] 王亦优
📃 [ 更新 ] 2024.6.10
❌ [ 勘误 ] /* 暂无 */
📜 [ 声明 ] 由于作者水平有限，本文有错误和不准确之处在所难免，
本人也很想知道这些错误，恳望读者批评指正！| 📜 参考资料 Microsoft. MSDN(Microsoft Developer Network)[EB/OL]. []. . |
