- 💬 写在前面：回顾我们的目标是为 F- 语言设计一个完备但不完全的类型系统，本章我们探讨的主题是类型系统的完备性。
目录
0x00 类型系统的不完备性
0x01 为什么推导树推导失败？
0x02 实现类型系统
0x03 调整到类型系统
0x04 思考：强制程序员写类型还是自动推断类型？
0x00 类型系统的不完备性
完备性属性可以描述如下：如果 𝝓 ⊢ 𝒆 ∶ 𝒕 成立，则程序 𝒆 不会出现类型错误。
同时，如果该程序终止并输出 𝒗 作为结果，则 𝒗 的类型是 𝒕
（注意，𝝓 ⊢ 𝒆 ∶ 𝒕 并不保证程序一定会终止）
下面我们来讨论一下类型系统的 不完备性 (Incompleteness)。
可能存在一些程序，即使没有任何类型错误，我们的类型系统也无法接受。
存在这样的程序 𝒆，使得对于某个𝒗，𝝓 ⊢ 𝒆 ⇓ 𝒗 成立，但对于任何𝒕，𝝓 ⊢ 𝒆 ∶ 𝒕 都不成立。比如 if true then 1 else false，再比如 let f x = x in if (f true) then (f 1) else 2
我们当前的类型系统不支持这种多态性：稍后我们将简要讨论这个问题。
0x01 为什么推导树推导失败？
不能同时是
和
。
即使将 保持为
类型也不能解决这个问题。
0x02 实现类型系统
到目前为止我们讨论过的类型规则 (𝚪 ⊢ 𝒆 ∶ 𝒕) 是我们类型系统的规范。
对于给定的程序 𝒆，如果存在某个类型 𝒕 使得 𝝓 ⊢ 𝒆 ∶ 𝒕 成立，那么我们的类型系统必须接受 𝒆。
如果不存在这样的类型 𝒕，则我们的类型系统将不接受 𝒆。
现在，让我们考虑如何实际实现它，我们应该如何编写这个类型系统的代码？
回顾一下解释器，当我们编写 F- 解释器时，语义可以很容易地通过递归实现。
我们可以直接将 𝝆 ⊢ 𝒆 ⇓ 𝒗 的定义翻译成代码 (就像下面的例子那样)
对于类型系统，我们是否也可以这么做呢？
let rec evalExp(exp: Exp) (env: Env) : Val =
match exp with
| LetIn(x, e1, e2) ->
let v1 = evalExp e1 env
evalExp e2(Map.add x v1 env)
| ...0x03 调整到类型系统
你可能会认为我们可以做同样的事情，对大多数情况而言，这是有效的。
如下例所示，注意下面的代码 (看起来是不是很类似于解释器的代码？)：
let rec typeOf (exp: Exp) (tenv: TyEnv) : Typ =
match exp with
| LetIn (x, e1, e2) ->
let t1 = typeOf e1 tenv
typeOf e2 (Map.add x t1 tenv)
| ...0x04 思考：强制程序员写类型还是自动推断类型？
下面的类型规则中，我们无法通过递归来确定参数类型 。
在绘制推导树时，你可以用 "直觉" 来理解，但计算机是如何做到的？
let rec typeOf (exp: Exp) (tenv: TyEnv) : Typ =
match exp with
| LetFunIn (f, x, e1, e2) ->
let ta = ??? // 这里我们应该做啥？
let tr = typeOf e1 (Map.add x ta tenv)
typeOf e2 (Map.add f (ta → tr) tenv)
| ...一个可能的解决方案是 —— 强制程序员写出参数类型（let f (x: int) = ...）
"程序员何必为难程序员……"
不然的话，我们就需要一个算法来 自动推断类型 了，我们会在下一章进行讲解！
📌 [ 笔者 ] 王亦优
📃 [ 更新 ] 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 |
