Hindley-Milner可以返回多个错误吗？

Question

我对类型推断还很陌生，我想知道是否有什么好的扩展或论文可以让HM允许出现多个错误。

我可能遗漏了一些东西，但是如果存在统一错误，类型检查器可以在类型上下文“有毒”的情况下继续进行吗？

Answer 1

您可以通过忽略全部或部分违规的统一来从统一错误中恢复(包括发生检查失败)，并且可以通过使用新的类型变量键入标识符来从“未知标识符”错误中恢复。安排不“毒害”您的类型上下文是很容易的，即使您决定部分地处理特定的统一。

更具体地说，如果您正在实现某个版本的Algorithm J，那么粗略地说，程序文本完全决定了递归构造的“指令”序列来转换类型上下文。唯一可能失败的“指令”是在Var中查找未知标识符的polytype和在App中查找统一步骤。其他任何事情(在Var中实例化polytype，在App和Abs中创建新的类型变量，在Let中将monotype泛化为polytype，或者在Abs和Let中扩充类型上下文)都不可能失败，前提是类型上下文表示实际上没有损坏。

在将类型变量序列绑定到单一类型之前，统一的“指令”通常被实现为一个递归，该递归匹配原始类型构造函数(函数箭头(->)、对、列表或您所包含的任何其他原始类型)。根据您表示统一结果的方式，您可能会发现，在任何类型构造函数不匹配时(尝试统一函数和对等)，只需修剪递归即可。跳过任何未通过发生检查的绑定尝试将使您的类型上下文处于有效状态，因此类型检查可以继续，并可能生成其他信息性错误。