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

Question

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

了解这个背景的最佳方法是什么？

Answer 1

类型理论是一个很大的领域.首先,"类型"一词在计算机科学中是一种用词不当,原因有几个,即使它们主要用于相同的基本思想.在许多情境中出现了类型,哲学,计算机科学和数学,主要是出于同样的原因.数学类型的起源来自试图使集合论形式化并遇到细胞悖论,尽管计算机科学中出现了类似的悖论.(例如,我喜欢指出吉拉德在这个问题上的悖论).

您可能在当前时刻解释类型的方式是一种在70年代到90年代在计算机中流行的想法:类型是一种轻量级的流量不敏感分析,它允许我们对我们编写的程序做出简明的逻辑保证.类型可以用于此,但实际上您可以将它们一直带到编码高阶逻辑,其中程序是证明.一旦你到这里,你可以拿一个证明,提取计算组件,并把它变成一个计算"正确"结果的程序(关于你证明的定理).

您可以从这里走几条路:

• 抓住Ben Pierce的类型和编程语言的副本. 这是对的书来读,并在计算机科学的最好的书之一.它涵盖了我们为什么需要类型的理论,以及我们如何使用它们来强制执行对程序的约束!
• 学习一种定期使用类型的语言来强制执行程序语义.特别是,您可以学习OCaml,Haskell或Agda.Haskell目前似乎是最好的选择,它有相当多的扩展,使它真正具有吸引力,并且是一个非常活跃的用户社区.事实上,在顶级会议上发布的结果很快就会在短短几年内在社区中广泛使用!
• 学习使用基于建构类型理论的定理证明器.在我看来,这是理解类型理论背后真正问题的唯一真实方法.有很多不错的选择,尽管Coq和Isabelle现在是真正的竞争者.Coq有一个很大的优势:Ben Pierce也有一本涵盖它的书! 软件基金会深入介绍了编程语言的一些理论,你真的可以用它来证明.

您可能还想查看一些相关字段:

• 类别理论是数学,往往是这些东西的基础.例如,可以对这些语言中给出的(共)归纳数据类型进行分类解释.
• 逻辑.学习一些好的旧传统逻辑可能​​会有所帮助,尽管我相信你所需要的大部分内容都可以通过Ben Pierce的SF书来阅读.然而,仍然有很多参考旧系统(后续微积分和自然演绎).
• 了解Haskell社区!正如我所说,它们正在迅速发展,并对计算机科学中的类型提出了深刻的问题.
• 编程语言中的伟大作品有很多很棒的文章!

除了这个之外我还有一些很好的建议,但我肯定从Ben Pierce的书开始(我从未真正进入后续书"类型和计算机科学的高级主题",但这也许也很有趣给你).特别是,我记得"自动推理手册"有一篇关于高阶类型理论的伟大文章.

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