类型检查算法

Question

我正在启动有关类型检查算法的个人书目研究，并想要一些提示。哪些最常用的类型检查算法，策略和一般技术是什么？

我对复杂的类型检查算法特别感兴趣，这些算法以广为众所周知的静态类型语言（例如C ++，Java 5+，Scala或其他）实现。即，由于基础语言的非常简单的键入（例如Java 1.4及以下），它的类型检查算法不是很简单。

我本身对特定语言X，Y或Z不感兴趣。无论其针对的语言如何，我都有感兴趣的字体检查算法。如果您提供了一个答案，例如“ Language L从未听说过哪些是强烈键入的，并且键入为复杂的是一种类型检查算法，该算法通过使用算法Z检查X和Y来进行A，B和C，或者“策略X和Y用于Scala和用于C＃的A的变体Z非常酷，因为R，S和T功能以这种方式起作用”，因此答案很好。

Answer 1

大多数研究实际上并未发布用于完整吹制编程语言的类型检查算法。您会发现针对完整编程语言的大部分类型系统的一些形式化，例如 Drossopoulou和Eisenbach for Java 或者 Nipkov等人在C ++上的工作. 。但是，更常见的是，您只会找到该语言某些核心部分的类型系统（轻量级Java是一个例子）或语言的核心概念，例如 Scala的本地类型推理方法.

在POPL和ICFP等会议中，您会发现许多类型的特定类型系统检查算法，以及诸如 双向 和 三个方向 类型检查。

更一般地，您可能需要了解 Damas-Milner算法, ，局部类型推理，双向和三个方向类型检查，并通过以下论文中的参考文献并使用Google Scholar来从那里扩展，并使用Google Scholar查找哪些论文引用了这些论文并建立在所描述的方法上。另外，如上所述，POPL，ICPF，ESOP甚至Ecoop和Oopsla等会议将与您的任务相关。

Answer 2

一个基本工具是 属性语法. 。您也许无法与他们一起想象的所有邪恶的事情，但它们是一个很好的起点。

从本质上讲，您可以自上而下地浏览程序的抽象语法树和/或自下而上，并传递信息。因此，例如，您可以向下传递全局范围类型信息（例如类及其成员），并递归确定表达式的类型，即自下而上，将结果类型向上传递。

在幻灯片中找到一些解释和示例 这里 （第5章）。