36

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

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

4

1 回答 1

60

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

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

您可以从这里走几条路：

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

您可能还想研究一些相关领域：

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

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

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

于 2012-06-15T19:54:01.703 回答