深入研究类型系统和类型理论答案

【问题标题】：Intense study of type systems and type theory深入研究类型系统和类型理论
【发布时间】：2017-01-13 07:14:31
【问题描述】：

我想了解类型背后的实际理论，而不是仅仅了解一些现有语言的最新实际变化（例如，不仅仅是 Haskell 或 Scala 的类型系统如何工作）。

获取此背景的最佳方法是什么？

【问题讨论】：

【解决方案1】：

类型理论是一个很大的领域。首先，术语“类型”在计算机科学中是一种用词不当，出于几个原因，尽管它们主要用于相同的基本概念。出于相同的原因，类型已经出现在许多环境中，如哲学、计算机科学和数学。数学中类型的起源来自于试图将集合论形式化并遇到一些细微的悖论，尽管类似的悖论也出现在计算机科学中。（例如，我喜欢指出 Girard 的悖论）。

目前你可能解释类型的方式是一个在 70 年代至 90 年代计算机中流行的想法：类型是一种轻量级的流不敏感分析，它允许我们对我们编写的程序做出简明的逻辑保证。类型可以用于此，但您实际上可以将它们一直用于编码更高阶的逻辑，其中 programs 是 proofs。到这里后，您可以进行证明，提取计算组件，并将其转换为计算“正确”结果的程序（关于您证明的定理）。

你可以从这里走几条路：

获取一份 Ben Pierce 的 Types and Programming Languages. 的副本，这是值得阅读的书，也是计算机科学领域最好的书籍之一。它涵盖了我们为什么需要类型的理论，以及我们如何使用它们来对我们的程序实施约束！
学习一门可以定期使用类型来强制执行有关程序语义的语言的语言。特别是，您可以学习 OCaml、Haskell 或 Agda。 Haskell 似乎是目前最好的选择，它有相当多的扩展使其非常有吸引力，并且是一个非常活跃的用户社区。事实上，在顶级会议上发布的结果在短短几年内就在社区中得到广泛使用是很常见的！
学习使用基于构造类型理论的定理证明器。在我看来，这是了解类型理论背后真正问题的唯一真正方法。有很多不错的选择，尽管 Coq 和 Isabelle 现在是真正的竞争者。 Coq 有一个很大的优势：Ben Pierce 也有一本书涵盖了它！ Software Foundations 深入涵盖了编程语言中的大量理论，您真的可以使用它证明事物。

您可能还想查看一些相关领域：

类别理论是这些东西的基础数学。例如，可以对这些语言中给出的（共）归纳数据类型进行分类解释。
逻辑。学习一点古老的传统逻辑可能会有所帮助，尽管我相信您可以通过阅读 Ben Pierce 的 SF 书获得您需要的大部分内容。但是，仍然有很多参考旧系统（连续微积分和自然演绎）。
了解 Haskell 社区！正如我所说，他们正在迅速行动，并提出有关计算机科学类型的深刻问题。
Great Works in Programming Languages 有很多很棒的文章！

除此之外，我还有一些很好的学习建议，但我肯定会从 Ben Pierce 的书开始（我从来没有真正进入过后续书籍“类型和计算机科学的高级主题”，但那是也许你也很有趣）。特别是，我记得《自动推理手册》中有一篇关于高阶类型理论的精彩文章。

P.s.，我确信这个问题的答案是具体的，“获得博士学位。在编程语言、哲学或逻辑方面......”;-)

【讨论】：

≈½ 周后找到答案，我只是在阅读本杰明的书，我不得不说它不是很好。首先，理解这本书需要成熟的数学符号（除了特定论文或书籍的作者定义的符号之外没有符号的想法）。其次，我只是在阅读 λ-calculi 章节，作者要么对自己的符号解释不好，要么有些公式是错误的。顺便说一句，我确实知道 λ-calculi！
我不同意。我还没有看到更容易理解的类型理论介绍性处理。经济地定义所有符号然后使用它以“引导式”风格定义其余类型，而不参考传统符号（例如，模型理论）的想法是一个核心 i> PL 中的想法。你能指出错误的公式吗？我以前教过这本书，我相信作者很想知道。
啊，好吧，我确实理解了我要为 （第 55 页底部的那个） 抱怨的符号，但 FWIW 我认为它花了大约 15- 20 分钟，而我正在思考/写下这似乎有什么问题。总的来说，这本书给我的感觉是作者还没有说什么重要的东西，所以我仔细学习了这个符号，但它从来没有发生过。但很可能，这就是类型论。现在，对我来说，直接练习 Haskell 和学习类别理论似乎更有用（我知道一点 atm，并且认为它很有用）。