关键字：static checking, dynamic checking, first-order type system, second-order type system, strongly checked language, weakly checked language, type safety, polymorphism, subtype

    推荐：★★★★
    难度：★★★

    在线地址：http://lucacardelli.name/Papers/TypeSystems.pdf

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

    Type Systems
    作者是Luca Cardelli。

    之所以看这本书，
    是因为对类型理论认识实在是太混乱了。

    什么是静态类型检查，
    什么是动态类型检查，
    什么是类型安全的，
    什么是类型可靠的。

    认识一直很模糊。

    无类型lambda演算，
    类型化的lambda演算，
    具有多态类型的语言，
    具有子类型的语言。

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

    本书虽然薄，
    但是可以帮助建立大局观。

    其实，一开始看的时候，
    对里面的某些符号不太了解， 例如：Type Systems - 图1

    于是，后来又看了《数理逻辑》，
    这才明白了本书末尾一段的深意，
    类型理论是形式逻辑的一个分支。

    书中还对first-order类型系统，
    second-order类型系统，
    进行了介绍。

    唯一不足的是，没有点破逻辑与类型建立关系的线索，
    即，Curry-Howard同构。

    最后本文以书中的原话结尾，
    不学习类型系统，就无法讨论程序的类型是什么，
    正如，不学习BNF就无法讨论程序的语法一样。