关于类型安全

[ice1000]

https://github.com/FrankHB/pl-docs/blob/master/zh-CN/typing-vs-typechecking.md#%E7%B1%BB%E5%9E%8B%E5%AE%89%E5%85%A8type-safety

这里写的类型安全感觉应该更准确地叙述为 语义的可靠性 (semantic soundness)。 类型安全的一个版本的定义 (又叫 type soundness) 是 progress and preservation。

[ice1000]

https://langdev.stackexchange.com/q/3565/40

[FrankHB]

这里说的是一个未决的口水话题。一般的所谓“安全”是指某种算法过程可以明确分析的、符合用户期望的程序的良好性质，非常宽泛。技术以外更多实质问题是谁来定义什么叫“安全”。“安全”与否带有相当的主观性，以至于在很多上下文中是可以商量的，比如 Rust 大约不晚于 2014 年决定把 leak 排除出 memory safety ，一个现实理由是严格的保证太麻烦了（另外还有 leak 怎么定义的问题，不过这个可以抄 [Cl98]）。同样地，type safety 其实可以涵盖许多类似的导出性质。除了通过类型系统保证的安全（C++ default RAII ，Rust lifetime 等）外，还有排除一些拒绝服务攻击的算法复杂度安全等。

可靠性是一类通过断言两个形式系统上的陈述的判断的互操作性保证预期的性质，其中一个系统描述程序的静态表示，另一个系统描述程序的执行。因为（至少直觉上）这种性质对任意非平凡（全是废话）的形式系统上总是可以给出一些符合用户预期的非平凡陈述，它能够作为安全性的实现。类型可靠性是在形式系统中引入类型的一种可靠性。但作为安全性的类型安全性，通常要超过这个范畴，因为纯粹的可靠性本身不涉及断言的前提和导出假设的可用性——可靠性能保证一些通过类型检查证明的性质符合预期，但具体是什么预期，原则上没有保证（依赖用户的主观性）。而这里批判的论述其实已经提出了一些预设的立场，并不只是可靠性。而这部分讨论的中心也是质疑这种钦点具体应当具有何种前提、满足何种目的的定义，并不具有充分的普适性，更不足以代表类型安全性。

所以我不认为这段的核心观点有问题。但应该如何以技术语言添加这些解释，以及补充可靠性和安全性的关系，是可以改进的。

不过说到语义可靠性，其实还有更大的坑……就是之前所说的类型的本体论意义。如 TAPL 所说，类型系统在这里充当的很大程度是语法的系统（即便通常语言规范中会把类型系统描述的规则作为程序的语义规则），它经常只保证相对一小部分可以无视程序执行性质，除了直接硬编码具体名义类型的语义规则，任何类型在演绎中很大程度只是个符号（“平凡的”），它在程序中起到的作用主要取决于用户程序为其指派的含义，语言规则不怎么关心这样的类型“是什么”。于是，所谓的可靠的语义，只是保证少数的预设的语法系统中的规则能够演绎的结论上的性质（即便这里允许可靠性混入了预设立场包含了具体的前提），这对通用目的语言需要类型系统做的（实用的）可靠性非常有限。就如这里 progress 对实际的程序是很小的一个性质一样。尽管它可以作为一个实例（引入并发构造的某种 lambda 演算方言上）的实现，它距离用户的期望太远了。要是允许用户扩展语言、修改这些前提呢？有的规则可能继续保持，有的可能被破坏。更重要的是，不管是 fork 出新的方言还是在原有语言规则上迭代和合并，新的可靠性对可靠性是否足以被视作安全性（不要忘了这里有不小的主观性），是否能满足预期用户的需要，通常是没法预料的。

何种程度的类型系统设计中的类型可以被视为程序的形式语义的必备部分，也是有疑问的（但原则上这里又不该具有多少主观性，否则这个考虑问题基本没用）。这个意义上，有多少部分的类型可靠性可以无疑义地被作为结论放在语义范畴，也是有疑问的。

所以可靠性在这里的实用上是个更大的坑（开放性问题），提出来也并不会让观点更明确，反倒会多出一堆问号（于是可能更适合作为思考题）。这算是我当时一直不想在这里太正式展开讨论的一个原因。