对 Haskell 类型推断感到困惑

Posted 2023-03-28

【中文标题】对 Haskell 类型推断感到困惑

【英文标题】：Confusing about Haskell type inference

【发布时间】：2016-04-13 02:39:23

【问题描述】：

我刚刚开始学习 Haskell。由于 Haskell 是静态类型的并且具有多态类型推断，所以恒等函数的类型是

id :: a -> a

suggesting id 可以取任意类型作为参数并返回自身。我尝试时效果很好：

a = (id 1, id True)

我只是假设在编译时，第一个id是Num a :: a -> a，第二个id是Bool -> Bool。当我尝试以下代码时，它给出了一个错误：

foo f a b = (f a, f b)
result = foo id 1 True

它表明a的类型必须与b的类型相同，因为它可以正常工作

result = foo id 1 2

但是id的参数的类型是不是可以是多态的，所以a和b可以是不同的类型？

【问题讨论】：

是***.com/questions/32496864/…你想要什么？

@haoformayor 不，这是关于forall，我认为不是单态限制。 foo 的推断类型必须是 (forall a . a -> a) -> a -> b -> (a, b)，但 AFAIK haskell 从不推断具有 forall 的类型（我认为称为 rank-2 类型？），即使禁用了单态限制。

啊，这就是答案。 ghc 推断出 rank-1 类型 forall a b. (a -> b) -> a -> a -> (b, b)，但您确实想要 (forall a. a -> a) -> a -> b -> (a, b)。

我真的没有时间来充实这个答案，但如果你有时间，请随时这样做，@haoformayor。

【参考方案1】：

好吧，这是 Haskell 类型系统的一个怪异怪异的角落。这里的问题是有两种方法可以对你的函数foo进行类型推断。

-- rank 1
foo :: forall a b. (a -> b) -> a -> a -> (b, b)
foo f a b = (f a, f b)

-- rank 2
foo' :: (forall a. a -> a) -> a -> b -> (a, b)
foo' f a b = (f a, f b)

第二种是你想要的，但第一种是你得到的。第二种类型，正如 amalloy 指出的那样，是 rank-2 类型（我们将忽略这两者的含义，但如果您想对排名有很好的解释，请阅读 "Practical type inference for arbitrary-rank types" 中的介绍 - 不要被作为开头的 PDF 文件的学术性质是可访问且清晰的）。

我们暂时推迟对高阶类型的定义，只是说问题在于 GHC 无法推断出 rank-2 类型。引用论文：

众所周知，完整的类型推断对于更高级别（不可预测的）类型系统是不可判定的，但实际上程序员更愿意添加类型注释来指导类型推断引擎，并记录他们的代码....

Kfoury 和 Wells 表明，对于 rank ≤ 2 的可类型性是可判定的，而对于所有 ≥ 3 的秩是不可判定的（Kfoury & Wells，1994）。对于 rank-2 片段，同一篇论文给出了一种类型推断算法。这种推理算法有些微妙，不能与用户提供的类型注释很好地交互，而且据我们所知，还没有在生产编译器中实现。

Undecidable 意味着不存在总是导致正确的是或否决定的算法。所以你有它：不可能推断出 3 级或更高级别的类型，而且很难推断出 2 级的类型。

现在，回到 2 级。(forall a. a -> a) 使它成为 2 级。 There's already an excellent Stack Overflow question about what the forall keyword means 所以我会推荐你​​，但基本上这意味着你可以在表达式 (f a, f b) 中调用 f a 和 f b 而 拥有 a 和 b 是不同的类型，这是你最开始想要的，在这一切乱七八糟之前。

最后一件事：您通常在 GHCi 中看不到 foralls 的原因是任何位于最外层范围的 foralls 都被忽略了。所以forall a b. (a -> b) -> a -> a -> (b, b) 等价于(a -> b) -> a -> a -> (b, b)。

总的来说，这是语言的一个痛点，解释得不好。

（向 cmets 中的@amalloy 致敬。）

【讨论】：

值得注意的是，这两种类型都不比另一种更通用。每个都可以以另一个不能的方式使用。所以foo f a b = (f a, f b) 孤立地看待实际定义的功能是模棱两可的；目前，通过采用 rank-1 类型的解释来解决歧义。在 GHC 具有完美的 2 级推理且没有历史包袱更喜欢 1 级解释的假设世界中，您可能需要添加一些确定选择的内容，因为这不是我们想要的那种东西编译器为您选择。

顺便说一句，forall a. a -> a 类型只包含一个非底部值 (id)，因此 foo' 本质上与 (,) 同构。