收藏
Types and Programming Languages - Benjamin C. Pierce

Types and Programming Languages

Benjamin C. Pierce

出版社

The MIT Press

出版时间

2002-02-01

ISBN

9780262162098

评分

★★★★★

标签

类型系统编程语言programming计算机科学

书籍介绍
这几乎不是普通意义上的编程书，而是一套训练形式化思维的体操。它从最简单的无类型 lambda 演算起步，一步步往语言里注入类型、子类型、引用，每一步都先给出精确的形式化定义，再用数学证明（尤其是三种数学归纳法）去验证这门语言的性质。读者反复提到的关键词是 proof——不做证明就谈不上真正理解，STLC 的强规范化在书里一笔带过，却需要自己补上知识储备才能看清门道。它适合那些不满足于'会用语言'、而想知道'语言为什么这样设计'的人：类型系统如何把错误行为挡在编译期、如何保护抽象的完整性，都在严密的推导中变得可被把握。
AI导读
核心看点
  • 系统介绍类型系统与编程语言基础理论
  • 结合编程实例，采用务实的操作视角
  • 涵盖从简单语言到子类型等高级特性
读者共识
  • 公认的经典教材，内容严谨且全面
  • 难度较大，后半部分如递归类型极难
  • 不做证明难以真正理解，需反复研读
精彩摘录
  • "Q: Why bother doing proofs about programming languages? They are almost always boring if the definitions are right. A: The definitions are almost always wrong."
  • "n one end of the spec- trum are powerful frameworks such as Hoare logic, algebraic specification languages, modal logics, and denotational semantics. These can be used to express very general correctness properties but are often cumbersome to use and demand a good deal of sophistication on the part "
  • "At the other end are techniques of much more modest power—modest enough that automatic checkers can be built into compilers, linkers, or program analyzers"
  • "The more abstract focuses on connections between various “pure typed lambda-calculi” and varieties of logic, via the Curry-Howard correspondence"
  • "they can categorically prove the absence of some bad program behaviors, but they cannot prove their presence,"
  • "type systems are also used to enforce higher-level modularity properties and to protect the in- tegrity of user-defined abstractions."
  • "Chains can be either finite or infinite, but we are more interested in infinite ones, as in the next definition"
  • "The mathemati- cal foundations of inductive reasoning will be considered in more detail in Chapter 21, where we will see that all these specific induction principles are instances of a single deeper idea."
用户评论
上TAPL的时候认认真真把这本书看了一遍，收获很多，而且课程拿了 A+开心～
跳过了各种证明 ...
书是挺好的，但是越来越读不懂了(2015/3-2015/7)
内容很全很丰富，还要多刷几次！
在皮尔斯荣膺 SIGPLAN 杰出教育奖之际，我终于把 TAPL 读完了。全书从 STLC 一直讲到了 F-omega-sub，中间还通过余归纳讲解了递归类型，基本上覆盖了依值类型之外的常见类型论，而且元理论上的性质几乎都附有纸笔证明。皮尔斯对 OOP 也是真爱，引入子类型之后有整整四章做对象建模的案例分析。
数理逻辑回炉重造 😔
PL的经典入门书，打开了新世界的大门
没啥好说的，pl必读书。从16年开始反反复复看了差不多有三年。后面几章有点难，而且难点不在如何理解concept，而在这些concept到底在讲了一个啥？或者说在整个system中起到了哪些关键性的不可替代性的作用。
得做proof啊！不做proof怎么可能懂 哭泣 STLC的strong normalization 书里一下就过去了 在不同的知识储备下看感觉是完全不一样的。。。
The MIT Press的其他书籍查看全部

下载
收藏