haskell - 为什么 Haskell 变量在被模式匹配绑定(bind)时不是多态的？

Question

考虑在模式中引入的变量，例如 f在这个 Haskell 示例中:

case (\x -> x) of f -> (f True, f 'c')

由于 f 的两种不同用法，此代码会导致类型错误(“无法将预期类型 ‘Bool’ 与实际类型 ‘Char’ 匹配”)。 .它表明 f 的推断类型在 Haskell 中不是多态的。

但是为什么不应该 f是多态的？

我有两点比较:OCaml 和“教科书”Hindley-Milner。两者都建议 f应该是多态的。

在 OCaml 中，类似的代码不是错误:

match (fun x -> x) with f -> (f true, f 'c')

计算结果为 (true, 'c')类型为 bool * char .所以看起来 OCaml 与分配 f 相处得很好一种多态类型。

我们可以通过将事物剥离到 Hindley-Milner 的基础知识来获得清晰 - 带有“let”的 lambda 演算 - Haskell 和 OCaml 都是基于它的。当归约到这个核心系统时，当然没有模式匹配这样的东西。不过，我们可以画出相似之处。在“let”和“lambda”之间，case expr1 of f -> expr2更接近 let f = expr1 in expr2比 (lambda f. expr2) expr1 . "Case"和 "let"一样，在语法上限制 f绑定(bind)到expr1 , 而函数 lambda f. expr2不知道是什么f将绑定(bind)到，因为该函数对在程序中调用它的位置没有这样的限制。这就是为什么在 Hindley-Milner 中泛化 let 绑定(bind)变量而 lambda 绑定(bind)变量不是的原因。似乎允许对 let-bound 变量进行泛化的相同推理表明，模式匹配引入的变量也可以被泛化。

为了清楚起见，上面的例子是最小的，所以它们只显示了一个简单的模式 f在模式匹配中，但所有相同的逻辑都扩展到任意复杂的模式，如 Just (a:b:(x,y):_) ，它可以引入多个可以泛化的变量。

我的分析正确吗？特别是在 Haskell 中——认识到它不仅仅是简单的 Hindley-Milner 而不是 OCaml——我们为什么不概括 f 的类型？在第一个例子中？

这是一个明确的语言设计决定吗？如果是，原因是什么？ (我注意到 some in the community think that not even "let" should be generalized ，但我想设计决策早于那篇论文。)

如果在模式中引入的变量被制成类似于“let”的多态性，那会在很大程度上破坏与 Haskell 其他方面的兼容性吗？

Answer 1

如果我们将多态类型 ( forall x. t ) 分配给案例审查员，那么它不会匹配任何重要的模式，因此使用 case 毫无意义。 .

我们能否以其他有用的方式进行概括？不是真的，因为 GHC 缺乏对“命令式”实例化的支持。在您的 Just (a:b:(x,y):_) 示例中, 没有单个绑定(bind)变量可以具有多态类型，因为 Maybe , (,) , 和 []不能用这种类型实例化。

正如评论中提到的，一件事有效:具有多态字段的数据类型，例如 data Endo = Endo (forall a. a -> a) .但是，多态字段的类型检查在技术上并不涉及泛化步骤，它的行为也不像 let-泛化。

原则上，可以在很多点上进行泛化，例如甚至在任意函数参数(例如在 f (\x -> x) 中)。然而，过多的泛化会通过引入难以处理的高阶类型而阻碍类型推断。这也可以理解为通过删除 Unresolved 元变量来消除程序不同部分之间有用的类型依赖关系。尽管有些系统可以比 GHC 更好地处理更高级别的推理，但最值得注意的是 MLF ，它们也更复杂，并没有看到太多实际用途。我个人更喜欢根本没有静默的 let-generalization。