我在这里看到一些关于静态与动态类型的有趣讨论。由于编译类型检查、更好的文档化代码等原因，我通常更喜欢静态类型。但是，我确实同意，如果按照 Java 的方式完成，它们确实会使代码变得混乱，例如。
所以我即将开始构建我自己的函数式风格语言，类型推断是我想要实现的事情之一。我确实明白这是一个很大的主题，我并不是想创造一些以前没有做过的东西，只是基本的推理......
关于阅读内容的任何指示将帮助我解决这个问题？最好是更实用/实用的东西，而不是更理论的范畴论/类型论文本。如果那里有实现讨论文本，带有数据结构/算法，那就太好了。
我发现以下资源有助于理解类型推断，按照难度递增的顺序排列：
然而，由于最好的学习方法是做，我强烈建议通过编程语言课程的家庭作业来实现玩具函数语言的类型推断。
我推荐这两个可访问的 ML 作业，您都可以在不到一天的时间内完成：
这些作业来自更高级的课程：
不幸的是，关于这个主题的许多文献都非常密集。我也站在你的立场上。我从编程语言：应用程序和解释中获得了对该主题的第一次介绍
我将尝试总结抽象的想法，然后是我没有立即发现的细节。首先，类型推断可以被认为是生成然后解决约束。要生成约束，您需要遍历语法树并在每个节点上生成一个或多个约束。例如，如果节点是+运算符，则操作数和结果都必须是数字。应用函数的节点具有与函数结果相同的类型，依此类推。
对于没有 的语言let，你可以盲目地通过替换来解决上述约束。例如：
(if (= 1 2)
1
2)
在这里，我们可以说 if 语句的条件必须是布尔值，并且 if 语句的类型与其thenandelse子句的类型相同。由于我们知道1并且2是数字，通过替换，我们知道该if语句是一个数字。
事情变得令人讨厌的地方，我有一段时间无法理解的是处理 let：
(let ((id (lambda (x) x)))
(id id))
在这里，我们绑定id了一个函数，该函数返回您传入的任何内容，也称为身份函数。问题是函数参数的类型x在每次使用时都不同id。第二个id是 type 的函数a -> a，a可以是任何东西。第一个是类型(a -> a) -> (a -> a)。这称为 let 多态性。关键是以特定顺序求解约束：首先求解 的定义的约束id。这将是a -> a。然后，可以将类型的新的、单独的副本id替换到每个id使用位置的约束中，例如a2 -> a2and 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
我希望这有助于澄清一个有点模糊的世界。
除了函数式语言的 Hindley Milner 之外，另一种流行的动态语言类型推断方法是
abstract interpretation.
抽象解释的想法是为该语言编写一个特殊的解释器，而不是保持一个具体值（1、false、闭包）的环境，它适用于抽象值，也就是类型（int、bool 等）。由于它是在抽象值上解释程序，这就是为什么它被称为抽象解释。
Pysonar2 是 Python 抽象解释的优雅实现。Google 使用它来分析 Python 项目。基本上它用于visitor pattern将评估调用发送到相关的 AST 节点。访问者函数transform
接受将context在哪个当前节点进行评估，并返回当前节点的类型。
Benjamin C. Pierce 的类型和编程语言
终极版 Lambda，从这里开始。