实施types推断
我在这里看到关于静态和dynamictypes的一些有趣的讨论。 我通常更喜欢静态types，因为编译types检查，更好的文档代码等等。但是，我同意，如果按照Java的方式完成代码，它们会混淆代码。
所以我即将开始构build自己的函数式语言，而types推断就是我想要实现的东西之一。 我明白，这是一个很大的主题，我不是要创造一个以前没有做过的事情，只是基本的推理…
任何指示什么读取将帮助我与此？ 最好是更实用/实用的东西，而不是更多的理论类别理论/types理论文本。 如果有一个实现的讨论文本，数据结构/algorithm，这将是可爱的。
我发现以下资源有助于理解types推断，以增加难度的顺序：
- 免费提供PLAI ， 编程语言：应用和解释 ，草图基于统一的types推断的第30章（Type Inference）。
- 暑期课程将types解释为抽象值，将呈现优雅的评估者，types检查者，types重构者和使用Haskell作为元语言的推理者。
- EOPL ， 程序devise语言 精粹第7章（types）。
- 书籍TAPL ， types和编程语言的第22章（types重构），以及相应的OCaml实现。
- 第十三章（types重构） 新书DCPL ， 编程语言中的devise概念 。
- select学术论文 。
- Closure编译器的TypeInference是types推断的数据stream分析方法的一个例子，它更适合于Hindler Milner方法的dynamic语言。
然而，由于最好的学习方法是做，我强烈build议通过编程语言课程的作业分配来实现玩具function语言的types推断。
我推荐ML中的这两个可访问的作业，你们都可以在一天之内完成：
- PCF Interpreter （ 解决scheme ）进行预热。
- PCFtypes推理 （ 一种解决scheme ）实现algorithmW为Hindley-Milnertypes推断。
这些作业来自更高级的课程：
-
实现MiniML
-
多态，存在，recursiontypes（PDF）
-
双向types检测（PDF）
-
子types和对象（PDF）
不幸的是，关于这个问题的许多文献是非常密集的。 我也是在你的鞋子里。 我从编程语言：应用和解释中得到了我的第一个介绍
我会尽量总结抽象概念，然后是我没有发现的细节。 首先，types推断可以被认为是产生和解决约束。 要生成约束，您需要遍历语法树，并在每个节点上生成一个或多个约束。 例如，如果节点是“+”运算符，则操作数和结果都必须是数字。 应用函数的节点与函数的结果具有相同的types，依此类推。
对于没有“让”的语言，你可以盲目地通过replace解决上述约束。 例如：
(if (= 1 2) 1 2) 在这里，我们可以说if语句的条件必须是布尔型的，if语句的types和它的“then”和“else”子句的types是一样的。 既然我们知道1和2是数字，通过replace，我们知道“if”语句是一个数字。
在那些令人讨厌的事情，以及我一时无法理解的地方，正在处理让：
(let ((id (lambda (x) x))) (id id))
在这里，我们已经绑定了一个函数，返回你传入的任何东西，否则称为身份函数。 问题是函数的参数'x'的types在id的每个用法上是不同的。 第二个“id”是a-> a的函数，其中a可以是任何东西。 第一个来自（a-> a） – >（a-> a）这被称为let-polymorphism。 关键是要按特定顺序解决约束：首先解决对“id”定义的约束。 这将是一个 – > a。 然后，可以将新的单独的idtypes的副本代入用于每个地方的约束，例如a2-> a2和a3-> a3。
在线资源中不容易解释这一点。 他们会提到algorithmW或M，但不是解决约束条件下的工作方式，或者为什么它不禁止let-polymorphism：这些algorithm中的每一个强制解决约束的顺序。
我发现这个资源非常有助于将algorithmW，M和约束生成的一般概念联系起来。 它有点密集，但比许多更好：
research/techreps/repo/CS-2002/2002-031.pdf
许多其他的文件也很好：
http://people.cs.uu.nl/bastiaan/papers.html
我希望这有助于澄清一个有点模糊的世界。
除了function语言的Hindley Milner之外，另一个stream行的dynamic语言types推断方法是abstract interpretation 。
抽象解释的思想是为语言编写一个特殊的解释器，而不是保留一个具体值（1，false，闭包）的环境，它对抽象值（又名types（int，bool等））有效。 由于它是解释抽象值的程序，所以这就是为什么叫做抽象解释。
Pysonar2是Python的抽象解释的优雅实现。 它被Google用来分析Python项目。 它主要使用visitor pattern对相关的AST节点进行评估调用。 访问者函数transform接受当前节点将被评估的context ，并返回当前节点的types。
types和编程语言由Benjamin C. Pierce
Lambda终极，从这里开始。
