我对类型推断还是很陌生,想知道是否有任何好的扩展或论文允许 HM 允许多个错误。
我可能会遗漏一些东西,但是如果出现统一错误,那么类型检查器是否可以在类型上下文“中毒”的情况下继续进行?
我对类型推断还是很陌生,想知道是否有任何好的扩展或论文允许 HM 允许多个错误。
我可能会遗漏一些东西,但是如果出现统一错误,那么类型检查器是否可以在类型上下文“中毒”的情况下继续进行?
您可以通过忽略所有或部分有问题的统一从统一错误(包括发生的检查失败)中恢复,并且可以通过键入带有新类型变量的标识符来从“未知标识符”错误中恢复。即使您决定部分处理特定的统一,也很容易安排不“毒化”您的类型上下文。
更具体一点,如果您正在实现某个版本的算法 J,那么粗略地说,程序文本完全确定了一个递归构造的“指令”序列来转换类型上下文。唯一可能失败的“指令”是在 [Var] 中查找未知标识符的多型和在 [App] 中的统一步骤。其他一切(在 [Var] 中实例化多型,在 [App] 和 [Abs] 中创建新的类型变量,在 [Let] 中将单型泛化为多型,或在 [Abs] 和 [Let] 中增加类型上下文)不可能失败,假设类型上下文表示实际上没有损坏。
(->)
在将一系列类型变量绑定到单型之前,统一“指令”通常会被实现为匹配原始类型构造函数(函数箭头、对、列表或任何其他原始类型)的递归。根据您表示统一结果的方式,您可能会发现在任何类型构造函数不匹配(尝试统一函数和对等)处简单地修剪递归并跳过任何未通过发生检查的尝试绑定将离开您的类型上下文处于有效状态,因此类型检查可以继续并可能产生其他信息错误。