关键字：类型，构造逻辑，操作语义，lambda演算，子类型化，递归类型，多态
推荐：★★★★
难度：★★★★★
豆瓣链接：https://book.douban.com/subject/1318672/
类型，仿佛是附着在程序语言的语法上的一套逻辑系统，
用它可以推导或证明一些性质。
对于任何图灵完备的语言来说，排除运行时的所有错误，是不可判定的，
因此类型理论只是在某种程度上保障了安全性。
对软件进行测试，观察软件在给定用例情况下的结果，
这是对软件性质的不完全归纳，并不能证明在所有情况下都表现良好。
除了动态测试的办法，还可以对软件进行静态缺陷查找，
方法有很多，例如，静态代码分析，编译时代码缺陷查找，
形式化分析，缺陷模式匹配，等。
除了词法分析和语法分析等方法之外，
类型检验是编译时代码缺陷查找的一种常用办法。
本书首先从布尔和数的无类型演算系统开始，
通过形式化的结构归纳方法，定义了表达式的操作语义，
即，在公理和推导规则基础上进行逻辑证明。
不断的增加公理和规则，演算系统会越来越庞大，
但数学家们追求的是精简，lambda演算具有和图灵机等价的计算能力，
而在规则上又足够简洁。
于是紧接着介绍了无类型的lambda演算，定义了它的语法和操作语义，
以及lambda演算的一些扩充和变型。
类型是对值进行的分类，这些类别属性可以看做值的静态信息，
于是，整个系统，除了包含运行时表达式值的一些推导规则之外，
还包括了表达式的类型所满足的约束条件，
类型系统在程序运行之前，可以排除了一些符合语法但不是良类型的表达式。
根据简单类型化方法，第九章将类型信息加入到了无类型lambda演算中，
得到了简单类型的lambda演算，
也看到了类型理论与逻辑之间的Curry-Howard对应关系，
即，简单类型lambda演算的一个项（的存在性）是与它类型对应的一个逻辑命题的证明。
除了简单类型之外，系统F对应于二值构造逻辑，系统
对应高阶逻辑，
线性逻辑催生出了线性类型系统，模态逻辑广泛的应用。
为了便于使用，下文对简单类型进行了扩展，
引入了let绑定，序对，元组，列表，和类型等常用概念。
子类型化，递归类型，多态，高阶系统，是高级编程语言中一些常见的类型系统，
它们对应于不同的逻辑系统，对它们的介绍占了本书的大部分内容。
限于篇幅和个人水平，只评论到此，
本书读了好几年，也没有通读，有些章节看过多遍，时间长了又忘了，
仅从头开始看，印象中已不下五遍。
为了看懂它，补充一些逻辑学知识是必需的，
然而，最重要的是看清楚本书用到的一些逻辑学常用方法。
书中每个系统都有作者的ML语言实现，
务实的同学可以阅读源码。
好了，就到这里吧，
晚上忽然醒了，记下这些，以便将来轻装上阵。
若有收获，就点个赞吧
0 人点赞
