实现类型推断

Question

我看到这里有一些关于静态和动态类型的有趣讨论。我通常更喜欢静态类型，因为它可以进行编译时类型检查，代码文档化程度更高等等。但是，如果像Java那样实现，它们确实会使代码变得混乱。

所以，我即将开始构建自己的函数式语言，类型推断是我想要实现的其中之一。我确实明白这是一个大主题，我并不想创造以前没有做过的东西，只是基本的推断...

有什么指导可以帮助我完成这个功能吗？最好是一些实用的东西，而不是更加理论的范畴论/类型论文本。如果有一个实现讨论的文本，带有数据结构/算法，那就太好了。

- deepblue

---

正是我正在寻找的问题，还有一些很棒的答案！ - Paul Hollingsworth

Answer 1

我发现以下资源对于理解类型推断非常有帮助，按照难度递增的顺序排列：

1. 免费提供的PLAI书籍的第30章（类型推断）概述了基于统一的类型推断。
2. 暑期课程将类型解释为抽象值使用Haskell作为元语言，展示了优雅的求值器、类型检查器、类型重构器和推断器。
3. EOPL书籍的第7章（类型）。
4. TAPL书籍的第22章（类型重构），以及相应的OCaml实现recon和fullrecon。
5. DCPL新书的第13章（类型重构）。
6. 学术论文的选择。
7. Closure编译器的TypeInference是数据流分析方法的一个例子，该方法比Hindler Milner方法更适合动态语言。

然而，由于最好的学习方法是实践，我强烈建议通过完成编程语言课程作业来实现类型推断玩具函数式语言。

我推荐这两个易于理解的ML作业，您可以在不到一天的时间内完成：

1. PCF Interpreter（一个解决方案）进行热身。 2. PCF Type Inference（一个解决方案）实现算法W以进行Hindley-Milner类型推断。 这些任务来自更高级的课程：

1. 实现MiniML

2. 多态，存在性和递归类型 (PDF)

3. 双向类型检查 (PDF)

4. 子类型和对象 (PDF)

- namin

---

是我自己的问题还是PLAI的描述主要是不正确/不完整的？这个讲座增加了一些内容，但似乎仍然不足以使其正常工作。 - Rei Miyasaka

我也无法理解2012年版的PLAI书中的算法。约束列表中没有替代方法。相反，我实现了2003-7版本PLAI书中的类型推导算法，它似乎效果更好，并且很好地扩展到let-polymorphism。 - heykell

看来recon和fullrecon链接已经失效。gzip版本仍然可用：recon.tar.gz，fullrecon.tar.gz。 - Flux

我们有没有任何实现类型检查/类型推断的例子，从命令式语言的角度而不是函数式语言的角度来看？ - Lance

Answer 2

很遗憾，这个主题的大部分文献都非常晦涩难懂。我也曾经和你一样困惑。我第一次接触这个主题是通过《编程语言：应用与解释》这本书。

http://www.plai.org/

我会尝试概括抽象思想，然后解释一些不太明显的细节。首先，类型推断可以被看作是生成和解决约束条件。为了生成约束条件，需要递归遍历语法树，并在每个节点上生成一个或多个约束条件。例如，如果节点是一个+运算符，则操作数和结果必须都是数字。应用函数的节点与函数结果具有相同的类型，以此类推。

对于没有let的语言，可以通过替换来盲目地解决上述约束条件。例如：

(if (= 1 2) 
    1 
    2)

在这里，我们可以说if语句的条件必须是布尔类型，并且if语句的类型与其then和else子句的类型相同。由于我们知道1和2是数字，通过替换，我们知道if语句是一个数字。

当涉及到let时，事情变得棘手，这也是我一段时间无法理解的地方：

(let ((id (lambda (x) x)))
    (id id))

在这里，我们将id绑定到一个返回任何你传入的参数的函数上，也就是所谓的身份函数。问题在于函数参数x的类型在每次使用id时都不同。第二个id是类型为a -> a的函数，其中a可以是任何类型。第一个是类型为(a -> a) -> (a -> a)的函数。这被称为let多态。关键是按特定顺序解决约束条件：首先解决id的定义的约束条件，这将是a -> a。然后可以将id的类型的新、分离的副本替换到每个使用id的地方的约束条件中，例如a2 -> a2和a3 -> a3。

这在网上资源中并没有很清晰地解释。它们会提到算法W或M，但不会解释它们如何在解决约束条件方面工作，或者为什么它不会因为let多态而失败：每个算法都对解决约束条件进行排序。

我发现这个资源非常有帮助，可以将算法W、M和约束生成和解决的整个概念联系起来。它有点密集，但比很多其他资源都好：

http://www.cs.uu.nl/research/techreps/repo/CS-2002/2002-031.pdf

其他的论文也很不错:

http://people.cs.uu.nl/bastiaan/papers.html

我希望这有助于澄清一个有些模糊的世界。

- Paul

Answer 3

除了Hindley Milner用于函数式语言的类型推断，另一种流行的动态语言类型推断方法是“抽象解释”。

抽象解释的思想是为语言编写一个特殊的解释器，而不是保持具体值(1、false、闭包)的环境，它使用抽象值，也就是类型(int、bool等)。由于它在抽象值上解释程序，所以被称为抽象解释。

Pysonar2是Python的抽象解释的优雅实现。它被Google用于分析Python项目。基本上，它使用访问者模式来将评估调用分派到相关的AST节点。访问者函数transform接受当前节点将被评估的context，并返回当前节点的类型。

- Wei Chen

Answer 4

《类型与编程语言》（Benjamin C. Pierce著）

- Scott Wisniewski

Answer 5

Lambda the Ultimate，从这里开始。

- Doug Currie