Type Systems

Review by [thzt]

• Rank: ★★★★
• Hard: ★★★
• Tag: static checking, dynamic checking, first-order type system, second-order type system, strongly checked language, weakly checked language, type safety, polymorphism, subtype
• Reviews:

最近读了一本40页的小书。

Type Systems

作者是Luca Cardelli。

之所以看这本书，

是因为对类型理论认识实在是太混乱了。

什么是静态类型检查，

什么是动态类型检查，

什么是类型安全的，

什么是类型可靠的。

认识一直很模糊。

无类型lambda演算，

类型化的lambda演算，

具有多态类型的语言，

具有子类型的语言。

它们分别属于什么类型系统。

本书虽然薄，

但是可以帮助建立大局观。

其实，一开始看的时候，

对里面的某些符号不太了解， 例如：|-

于是，后来又看了《数理逻辑》，

这才明白了本书末尾一段的深意，

类型理论是形式逻辑的一个分支。

书中还对first-order类型系统，

second-order类型系统，

进行了介绍。

唯一不足的是，没有点破逻辑与类型建立关系的线索，

即，Curry-Howard同构。

最后本文以书中的原话结尾，

不学习类型系统，就无法讨论程序的类型是什么，

正如，不学习BNF就无法讨论程序的语法一样。