实施类型推断
我在这里看到一些关于静态和动态类型的有趣讨论。 例如，由于编译类型检查，更好的文档化代码等，我通常更喜欢静态类型输入。但是，我确实同意，如果按照Java的方式完成代码，它们会混淆代码。
所以我即将开始构建自己的功能风格语言，并且类型推断是我想要实现的一件事情。 我确实明白这是一个很大的主题，而我并没有试图去创造以前没有做过的事情，只是基本的推理...
任何指示什么读取将帮助我与此？ 最好是更实用/实用的东西，而不是更多的理论类别理论/类型理论文本。 如果有一个实现讨论文本，数据结构/算法，这将是可爱的。
我发现以下资源有助于理解类型推断，以增加难度的顺序：
然而，由于学习的最佳方式是做，我强烈建议通过编程语言课程的作业分配来实现玩具功能语言的类型推断。
我建议在ML中使用这两种可访问的作业，这两种作业都可以在一天内完成：
这些作业来自更高级的课程：
实现MiniML
多态，存在，递归类型（PDF）
双向类型检测（PDF）
分类和对象（PDF）
不幸的是，关于这个问题的大部分文献都非常密集。 我也是在你的鞋子里。 我从编程语言：应用和解释中得到了我的第一个介绍
http://www.plai.org/
我会尽量总结一下抽象概念，然后是我没有立即发现的细节。 首先，类型推断可以考虑生成并解决约束条件。 要生成约束，您需要遍历语法树并在每个节点上生成一个或多个约束。 例如，如果节点是'+'运算符，则操作数和结果都必须是数字。 应用函数的节点与函数的结果具有相同的类型，依此类推。
对于没有'let'的语言，你可以通过替换盲目地解决上述约束。 例如：
(if (= 1 2)
1
2)
在这里，我们可以说if语句的条件必须是布尔型的，并且if语句的类型与其“then”和“else”子句的类型相同。 既然我们知道1和2是数字，通过替换，我们知道“if”语句是一个数字。
在那些令人讨厌的事情，以及我一段时间无法理解的事情中，我们正在处理让：
(let ((id (lambda (x) x)))
(id id))
在这里，我们将'id'绑定到一个函数，该函数返回您传入的任何内容，否则称为身份函数。 问题是函数参数'x'的类型在id的每次使用上都不相同。 第二个'id'是a-> a的函数，其中a可以是任何东西。 第一个来自（a-> a） - >（a-> a）这被称为let-polymorphism。 关键是要按特定顺序解决约束：首先解决'id'定义的约束。 这将是一个 - > a。 然后，可以将新的单独的id类型的副本替换为每个地方使用的“id”的约束条件，例如a2-> a2和a3-> a3。
这在网上资源中很难解释。 他们会提到算法W或M，但不是解决约束条件下的工作方式，或者为什么它不禁止let-polymorphism：这些算法中的每一个强制解决约束的顺序。
我发现这个资源非常有助于将算法W，M和约束生成的一般概念联系起来。 它有点密集，但比许多更好：
http://www.cs.uu.nl/research/techreps/repo/CS-2002/2002-031.pdf
许多其他的论文也很好：
http://people.cs.uu.nl/bastiaan/papers.html
我希望这有助于澄清一个有点模糊的世界。
除了功能语言的Hindley Milner之外，另一种流行的语言类型推断方法是abstract interpretation 。
抽象解释的思想是为语言编写一个特殊的解释器，而不是保留一个具体值（1，false，闭包）的环境，它适用于抽象值，也就是类型（int，bool等）。 由于它正在解释关于抽象值的程序，这就是为什么它被称为抽象解释。
Pysonar2是Python的抽象解释的优雅实现。 它被Google用来分析Python项目。 基本上它使用visitor pattern向相关的AST节点发送评估呼叫。 访问者函数transform接受将评估当前节点的context ，并返回当前节点的类型。
上一篇: implementing type inference
下一篇: Nunit & resharper test runner. How to get if the test is debugged or run