实现类型推断答案

【问题标题】：implementing type inference实现类型推断
【发布时间】：2010-09-29 18:07:01
【问题描述】：

我在这里看到了一些关于静态与动态类型的有趣讨论。由于编译类型检查、更好的文档化代码等原因，我通常更喜欢静态类型。但是，我同意如果按照 Java 的方式完成，它们确实会使代码变得混乱。

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

关于阅读内容的任何指示对我有帮助吗？最好是更实用/实用的东西，而不是更理论的类别理论/类型理论文本。如果那里有实现讨论文本，带有数据结构/算法，那就太好了。

【问题讨论】：

正是我正在寻找的问题，有一些很好的答案！

标签： compiler-construction functional-programming language-design type-inference

【解决方案1】：

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

the freely available book PLAI 的第 30 章（类型推断）编程语言：应用和解释，概述了基于统一的类型推断。
夏季课程Interpreting types as abstract values 展示了使用 Haskell 作为元语言的优雅的评估器、类型检查器、类型重构器和推理器。
the book EOPL 的第 7 章（类型），编程语言基础。
the book TAPL 的第 22 章（类型重构），类型和编程语言，以及相应的 OCaml 实现 recon 和 fullrecon。
the new book DCPL 的第 13 章（类型重构），编程语言中的设计概念。
Selection of academic papers。
闭包编译器的 TypeInference 是类型推断的数据流分析方法的一个示例，它更适合 Hindler Milner 方法的动态语言。

但是，由于最好的学习方式是做，我强烈建议通过编程语言课程的家庭作业来实现玩具函数语言的类型推断。

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

PCF Interpreter (a solution) 热身。
PCF Type Inference (a solution) 为 Hindley-Milner 类型推断实现算法 W。

These assignments 来自更高级的课程：

【讨论】：

只是我，还是 PLAI 描述在很大程度上不正确/不完整？ The lecture 增加了一点，但似乎仍然不足以让它工作。
2012版PLAI书里的算法我也拿不到。约束列表没有替换。相反，我在 PLAI 书的 2003-7 版本中实现了类型推断算法，它似乎工作得更好，并且也可以很好地扩展到 let-polymorphism。
recon 和 fullrecon 链接好像坏了。 gziped 版本仍然可用：recon.tar.gz、fullrecon.tar.gz。

【解决方案2】：

不幸的是，关于这个主题的许多文献都非常密集。我也站在你的立场上。我从 Programming Languages: Applications and Interpretation 中获得了对该主题的第一次介绍

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

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

【讨论】：

【解决方案3】：

除了函数式语言的 Hindley Milner，另一个动态语言类型推断的流行方法是 abstract interpretation.

抽象解释的思想是写一个特殊的语言的解释器，而不是保持一个环境具体值（1，false，闭包），它适用于抽象值，又名类型（int、bool 等）。因为它正在解释程序抽象值，这就是为什么它被称为抽象解释。

Pysonar2 是抽象解释的优雅实现对于 Python。 Google 使用它来分析 Python 项目。基本上它使用visitor pattern 来调度评估调用相关的 AST 节点。访客功能@987654321@ 接受将在其中评估当前节点的context，并且返回当前节点的类型。

【讨论】：

【解决方案4】：

Benjamin C. Pierce 的《类型和编程语言》

【讨论】：

【解决方案5】：

终极 Lambda，从 here 开始。

【讨论】：