类型系统和类型理论的深入研究

Question

我希望理解类型背后的实际理论，而不仅仅是学习某种现有语言中最新的实践变化（例如，不仅仅了解Haskell或Scala的类型系统如何工作）。

哪种方法是掌握这方面背景知识的最佳途径？

- user1311390

Answer 1

类型理论是一个很大的领域。首先，在计算机科学中，“类型”这个术语有一些误解，尽管它们通常用于相同的基本思想。类型在许多背景下出现过，包括哲学、计算机科学和数学等，大部分是由于相同的原因。类型在数学中的起源是为了形式化集合论并遇到琐碎的悖论，虽然计算机科学中也会出现类似的悖论（例如，我喜欢指出 Girard's 悖论）。

目前你可能对类型的解释是，在 70 年代至 90 年代期间，在计算机领域流行起来的一种想法：类型是一种轻量的流不敏感分析，允许我们对编写的程序做出简洁的逻辑保证。类型可以用于此，但实际上您可以将其推广到编码高阶逻辑，其中 程序 是 证明。一旦您进入这里，您就可以提取计算组件并将其转换为计算“正确”结果（关于您所证明的定理）的程序。

从这里可以走几条路：

• 获取 Ben Pierce 的《类型与编程语言》。这是阅读的关键书籍，也是计算机科学中最好的书籍之一。它探讨了我们为什么需要类型以及如何使用它们来强制执行程序约束！
• 学习使用类型定期强制执行程序语义的语言。特别是您可以学习 OCaml、Haskell 或 Agda。目前 Haskell 似乎是最佳选择，它具有许多扩展功能，使其非常吸引人，并且拥有一个非常活跃的用户社区。事实上，经常出现在顶级会议上发表的结果只需几年时间就流传到社区广泛使用！

学习使用基于构造类型理论的定理证明器。在我看来，这是了解类型理论背后真正问题的唯一途径。有许多好的选择，但Coq和Isabelle现在是最受关注的竞争者。 Coq有一个巨大的优势：Ben Pierce还写了一本涵盖它的书！软件基础深入探讨了编程语言中的很多理论，您可以使用它来证明想要的事情。

您可能还想学习一些相关领域：

• 范畴论是支持此类工具的数学理论。例如，可以采用范畴论解释给出在这些语言中(Co-)inductive数据类型。
• 逻辑。学习一些传统逻辑可能会有所帮助，尽管我相信您从阅读Ben Pierce的SF书中可以了解到大部分内容。但是，仍然会有很多引用旧系统（sequent calculus和natural deduction）。
• 学习有关Haskell社区的知识！他们正在快速发展，并针对计算机科学中的类型问题提出深刻的问题。
• 编程语言中的伟大作品有许多优秀的文章！

我还有一些很好的建议可以帮助您深入学习，但我肯定会从Ben Pierce的书开始（我从未真正了解过后续书籍“高级主题与类型和计算机科学”，但那也可能对您有趣）。特别是，我记得自动推理手册上有一篇关于高阶类型理论的好文章。

P.S.，我相信这个问题的具体答案是：“获得编程语言、哲学或逻辑的博士学位 ...”;-)

- Kristopher Micinski

---

大约半周之后，我刚刚读完了本杰明的书，不得不说它并不是很好。首先，理解这本书需要对数学符号成熟（即没有符号除了特定论文或书籍作者定义的符号）。其次，我正在阅读λ演算章节，但作者在解释自己的符号时要么表达不清，要么一些公式是错误的。顺便说一下，我确实知道λ演算！ - Hi-Angel

我尊重地不同意。我从未见过一种更易懂的类型理论入门教程。以经济定义所有符号，然后使用它们来定义其他类型的方法，而无需参考传统符号（比如模型论中借用的），是程序语言领域中的核心思想。能指出哪些公式有问题吗？我以前曾使用过这本书进行教学，我相信作者会很想知道。 - Kristopher Micinski

啊，好吧，我确实理解了我要抱怨的符号 *(在第55页底部)*，但是就我个人而言，我认为我花了大约15-20分钟思考/写下那个符号到底有什么问题。总的来说，这本书给我的感觉是作者还没有说出重要的东西，所以我正在仔细学习符号，但从未发生过。但可能，这就是类型理论。现在，对我来说，直接练习Haskell并学习范畴论 (我目前知道一些，并且认为它很有用) 更有用。 - Hi-Angel