如何理解 Hindley-Milner 类型系统中的算法 W？

【问题标题】：How to comprehend Algorithm W in Hindley–Milner type system?如何理解 Hindley-Milner 类型系统中的算法 W？
【发布时间】：2022-08-08 23:15:55
【问题描述】：

我正在研究算法 W。据我了解，算法 W 以 (Γ,expr) 作为输入，其中 Γ 是上下文，而 expr 是表达式。输出是一个替代σ。然后我可以使用替换 σ 将另一个 (Γ,expr) 作为 σ(Γ,expr)。

让我困惑的是下一步该做什么。由于 expr 可以有以下情况：变量、抽象、应用程序、条件、定点表达式和 let 表达式。

有不同的 expr 案例的目的是什么？下一步我应该做什么？

【解决方案1】：

算法 W 不仅返回一个替换，还返回一个类型 τ，这是从您从一开始就在算法中输入的表达式推断出的类型。

替换 S 是从类型变量 α 到类型 τ 的映射，因此替换不依赖于您所暗示的类型环境 Γ。

每个案例都是单独处理的（例如，应用程序使用统一，但您提到的另一个没有）并以递归方式互连。这是一些表达式的算法 W 的伪代码

【讨论】：