即使禁用了单态化限制，为什么 GHC 仍然推断出单态类型？

Question

这篇文章是由解决类型为`f = f (<*>) pure`所引发的，其中讨论了一个更复杂的例子，但这个例子也可以使用。

以下定义可以无问题编译：

w :: Integral a => a
w = fromInteger w

当然，这在运行时是不起作用的，但这并非问题所在。重点是`w`本身的定义使用了w :: Integer的一个特殊版本。显然，这是一个合适的实例化，因此可以通过类型检查。

然而，如果我们删除签名，则GHC推断出的不是上述类型，而只有具体类型：

w' = fromInteger w'

GHCi> :t w
w :: Integral a => a
GHCi> :t w'
w' :: Integer

当我看到这个时，我相当确定这是单态限制在起作用。众所周知，例如

i = 3

GHCi> :t i
i :: Integer

尽管i :: Num p => p是完全可行的。实际上，如果启用了-XNoMonomorphismRestriction，即禁用了单态限制，则会推断出i :: Num p => p。

然而，在w'的情况下，即使禁用了单态限制，仅推断出Integer类型。

为了排除这与默认值有关的可能性：

fromFloat :: RealFrac a => Float -> a
q :: RealFrac a => a
q = fromFloat q
q' = fromFloat q'

GHCi> :t q
q :: RealFrac a => a
GHCi> :t q'
q' :: Float

为什么多态类型无法推断？

- leftaroundabout

---

单态限制不仅适用于简单绑定吗（而且 w' = fromInteger w' 是递归的，因此不是简单的）？ - Alec

@Alec 可能是可能的，但为什么会出现像单态限制这样的东西呢？ - leftaroundabout

我可能有点迟钝，漏掉了什么，但是fromInteger的类型为(Num a) => Integer -> a，而且由于w'被用作fromInteger的输入，这难道不意味着Integer是它唯一可能的类型吗？事实上，我对具有多态类型签名版本的编译结果感到非常惊讶。（所以正如我所说，可能漏掉了什么。） - Robin Zigmond

@RobinZigmond Integer 显然是 w' 的唯一可能的 单态 类型，但是正如 w 所展示的那样，多态类型也完全可以。毕竟，多态类型可以被实例化为单态类型，只要它满足约束条件即可。 - leftaroundabout

Answer 1

多态递归（即一个函数在与它被调用时不同的类型上调用自身）总是需要一个类型签名。完整的说明在Haskell 2010报告的4.4.1节中：

如果一个变量f被定义而没有提供相应的类型签名声明，那么每个在其自己的声明组之外使用f的地方（参见4.5节）都被视为具有相应的推断出的或主要的类型。然而，为了确保类型推断仍然是可能的，定义出现和其声明组内对f的所有使用必须具有相同的单态类型（从中通过泛化获得主要类型，如4.5.2节所述）。

同一节还举了一个由类型签名支持的多态递归示例。

我的理解是，在存在多态递归的情况下，未辅助的类型推断通常是不可判定的，因此Haskell甚至不会尝试进行推断。

在这种情况下，类型检查器从以下开始：

w :: a

其中a是一个元变量。由于fromInteger在其自身声明中（因此在其声明组中）使用w作为参数调用，类型检查器将a与Integer统一。没有变量可以泛化。

稍微修改您的程序会出现不同的结果，原因相同：

v = fromIntegral v

根据你的原始推理，Haskell将推断出v :: forall a. Num a => a，将RHS上的v默认为类型Integer：

v :: forall a. Num a => a
v = fromIntegral (v :: Integer)

但是实际上，它以 v :: a 开始。由于 v 被传递给了 fromIntegral，所以它需要 Integral a。最后，它会将 a 泛化。最终，程序变成了

v :: forall a. Integral a => a
v = fromIntegral (v :: a)

- dfeuer

---

我的本科论文是关于一个简单的类型推断器，针对包括类型类和多态递归在内的 Haskell 的一个子集。一种非常简单的方法是限制多态递归的深度，最多到 k 层。大多数有用的多态递归情况都可以使用非常低的深度界限来推断（例如 k=1 或 k=2）。无论如何，Haskell 类型推断已经是不可判定的，这并不是它被禁止的唯一原因。另一个原因可能是性能问题，因为这肯定会使得类型推断 O(k·f(n)) 而不是 O(f(n))，因为您可能需要重新进行 k 次计算。 - Bakuriu

@Bakuriu，我非常确定Haskell 2010 没有 多态递归，但它具有完全的类型推断——基本上是 Hindley-Milner，再加上类型类和默认值。你有否认这一点的参考资料吗？至于一些有限的递归深度：这听起来可能是一个有用的扩展，但它与 Haskell 报告通常做的事情有着非常不同的风格。我会发现这样的功能对于发现多态递归代码的正确类型签名最有用。 - dfeuer

@Bakuriu，只是出于我的好奇心：使用有限的多态递归深度，可以推断出多少Data.Sequence？在这种情况下，当你说“深度”时，我不太确定你的意思。 - dfeuer

没有多态递归推断的原因正是因为它是不可判定的。这个决定早在 GHC 获得许多其他不可判定特性之前就已经有了。你可以相信我，那时我是 Haskell 委员会上的成员。 :) - augustss

据我所知，对于任何良好类型化的多态递归程序，都存在一个有限深度k，使得类型推断可以工作。问题在于，并不存在适用于每个程序的有限k。然而，当时我没有考虑其他Haskell扩展，因此如果您添加了类型族、函数依赖等内容，则可能不再成立。 - Bakuriu