ech*_*ata 6 ocaml haskell type-inference
考虑一个模式中引入的变量,例如f在这个Haskell示例中:
case (\x -> x) of f -> (f True, f 'c')
此代码导致类型错误("无法将预期类型'Bool'与实际类型'Char'匹配"),因为它有两种不同的用途f.它表明推断类型f在Haskell中不是多态的.
但为什么不应该f是多态的？
我有两点比较:OCaml和"教科书"Hindley-Milner.两者都表明f应该是多态的.
在OCaml中,类似的代码不是错误:
match (fun x -> x) with f -> (f true, f 'c')
这将(true, 'c')使用类型进行评估bool * char.所以看起来OCaml与指定f多态类型相处得很好.
我们可以通过使用"let"来解决Hindley-Milner - lambda演算的基本原理来获得清晰度 - Haskell和OCaml都是基于它的.当减少到这个核心系统时,当然没有模式匹配这样的东西.我们可以画出相似之处.与"让"和"拉姆达",case expr1 of f -> expr2是更接近let f = expr1 in expr2比(lambda f. expr2) expr1."case",就像"let"一样,在语法上限制f绑定expr1,而一个函数lambda f. expr2不知道f将绑定什么,因为函数对程序中的调用位置没有这样的限制.这就是为什么let-bound变量在Hindley-Milner中被推广而lambda-bound变量没有被推广的原因.看来,允许自由变量泛化的相同推理表明,模式匹配引入的变量也可以推广.
上面的例子是清晰度最小的,所以它们只f在模式匹配中显示一个简单的模式,但所有相同的逻辑扩展到任意复杂的模式Just (a:b:(x,y):_),如可以引入多个全部变量的变量.
我的分析是否正确？特别是在Haskell中 - 认识到它不仅仅是简单的Hindley-Milner而不是OCaml - 为什么我们不在f第一个例子中概括类型？
这是一个明确的语言设计决定,如果是这样,原因是什么？(我注意到社区中的一些人认为甚至"let"都不应该被概括,但我认为设计决定早于该论文.)
如果在模式中引入的变量是多态的,类似于"let",那么是否会以显着的方式破坏与Haskell的其他方面的兼容性？
如果我们将多态类型 ( forall x. t) 分配给案例审查者，那么它不会匹配任何非平凡的模式，因此拥有 是没有意义的case。
我们能否以其他有用的方式进行概括？事实并非如此，因为 GHC 缺乏对“命令式”实例化的支持。在您的示例中Just (a:b:(x,y):_)，没有一个绑定变量可以具有多态类型，因为Maybe、(,)、 和[]不能用此类类型实例化。
正如评论中提到的，有一件事是有效的：具有多态字段的数据类型，例如data Endo = Endo (forall a. a -> a). 然而，多态字段的类型检查在技术上并不涉及泛化步骤，它的行为也不像 let-泛化。
原则上，可以在许多点执行泛化，例如甚至在任意函数参数（例如在 中f (\x -> x)）。然而，过多的泛化会引入难以处理的高级类型，从而阻碍类型推断。这也可以理解为通过删除未解决的元变量来消除程序不同部分之间有用的类型依赖关系。尽管有些系统可以比 GHC 更好地处理更高阶的推理，尤其是MLF，但它们也复杂得多，并且没有看到太多实际用途。我个人更喜欢完全不进行沉默的泛化。