罗宾·米尔纳(Robin Milner)的具有参数多态性的类型系统比罗素和丘奇的系统有了显著的进步。这是使用类型变量的能力，使高阶Logica成为证明非平凡定理的实用工具。Hindley-Milner算法用于在定理证明器和其他几种函数式编程语言中自动推断类型。本教程将解释算法、类型系统和一些逻辑背景，并用标准ML实现。此实现纯粹是功能性的，旨在尽可能清楚地展示算法。上图旨在说明函数式语言可以用来表达数学和逻辑，使得数学表达式和程序表达式之间的对应关系可以像人们希望的那样精确。这有实际的后果。在实现算法iNML时，我在数学表达式中发现了几个错误和歧义。在构造算法的力学表达式的过程中，对这些问题进行了澄清。错误将通过编译器的语法和类型检查来检测，而歧义通过标准ML语义的规范来解决，这比我所见过的任何数学表示法的非正式描述都要精确得多。因为ML同样具有表现力，但是更精确，所以我认为ML程序比数学程序更好地描述了算法。标准ML是米尔纳的语言，它使用这种参数多态类型系统。类型推断算法实现的核心在于大约250行代码。它根本不包括任何显式类型注释，但是每个表达式的类型都是由编译器中的相同算法推断(并因此检查)的。该算法在1982年被Damas和Milner证明是可靠和完整的，并且证明在函数式程序的原则型方案中概述，我重新键入了这些证明，因为这篇论文写得很好，值得更广泛地阅读。源代码以纯文本SML源文件和html格式的标准ML格式提供。