Haskell的二阶多态编译错误

Question

抱歉，我只能用英语回答问题。

import Control.Monad.ST
import Data.STRef

fourty_two = do
  x <- newSTRef (42::Int)
  readSTRef x

以下代码可以在 GHC 下编译通过：

main = (print . runST) fourty_two -- (1)

但是这样不行：

main = (print . runST) $ fourty_two -- (2)

但是正如bdonlan在评论中指出的那样，这段代码可以编译：

main = ((print . runST) $) fourty_two -- (3)

但是，这段代码无法编译

main = (($) (print . runST)) fourty_two -- (4)

这似乎表明(3)只能编译因为中缀$的特殊处理，但这仍然无法解释为什么(1)能编译。

问题：

1) 我读了以下两个问题（第一个，第二个），并且我相信$只能用于单态类型。但我同样认为.也只能用于单态类型，因此将类似地失败。 为什么第一个代码可以成功编译，但第二个代码不能？（例如，GHC是否有适用于第一种情况的特殊规则，无法应用于第二个问题？）

2) 是否有当前的GHC扩展可以编译第二个代码？ （可能ImpredicativePolymorphism在某些时候可以做到这一点，但它似乎已被弃用，有什么替代品吗？）

3) 有没有办法使用GHC扩展定义类似`my_dollar`的东西，以执行$的操作，但也能处理多态类型，以使(print . runST) `my_dollar` fourty_two编译？

编辑：建议回答：

此外，以下内容无法编译：

main = ((.) print runST) fourty_two -- (5)

这与(1)相同，只是不使用中缀版本的.。

因此，看起来GHC对于$和.都有特殊规则，但仅适用于它们的中缀版本。

- Clinton

---

为了让它更有趣，( (print . runST) $ ) fourty_two 确实可以工作。 - bdonlan

那很有趣，但会让事情更加混乱！ - Clinton

@Daniel Wagner：这个问题略有不同。它询问为什么添加最终的 $ 会有所不同，而不是为什么用 . 替换第一个 $ 会有所不同。我的两个示例都使用 (a . b) 格式，与其他问题不同。那个问题可以通过 GHC 的特殊类型规则来回答，但似乎在这里并不适用。 - Clinton

糟糕，我甚至没有仔细阅读问题，以至于没有注意到您链接到了我提出的重复问题，并解释了为什么它不是重复的。抱歉！ - Daniel Wagner

要得到一个真正的答案，你需要找到一个对GHC类型检查算法非常熟悉的人。FYI，ghc-6.12.3编译除了（3）之外的所有形式，其中它抱怨无法将forall类型与（.）的第二个参数中的单态匹配。因此，在ghc-6和ghc-7之间的类型检查算法的更改改变了forall类型作为（.）和（$）的参数的处理方式。据我所知，从它们的类型来看，两者都不应该采用更高级别的类型，但这太不方便了，所以规则被弯曲了。 - Daniel Fischer

Answer 1

1. I'm not sure I understand why the second doesn't work. We can look at the type of print . runST and observe that it is sufficiently polymorphic, so the blame doesn't lie with (.). I suspect that the special rule that GHC has for infix ($) just isn't quite sufficient. SPJ and friends might be open to re-examining it if you propose this fragment as a bug on their tracker.

   As for why the third example works, well, that's just because again the type of ((print . runST) $) is sufficiently polymorphic; in fact, it's equal to the type of print . runST.

2. Nothing has replaced ImpredicativePolymorphism, because the GHC folks haven't seen any use cases where the extra programmer convenience outweighed the extra potential for compiler bugs. (I don't think they'd see this as compelling, either, though of course I'm not the authority.)

3. We can define a slightly less polymorphic ($$):

   {-# LANGUAGE RankNTypes #-}
   infixl 0 $$
   ($$) :: ((forall s. f s a) -> b) -> ((forall s. f s a) -> b)
   f $$ x = f x
   

   Then your example typechecks okay with this new operator:

   *Main> (print . runST) $$ fourty_two
   42
   

- Daniel Wagner

Answer 2

我对这个主题的权威性不太确定，但是我认为可能会发生以下情况：

考虑类型检查器在每种情况下所需执行的操作。 (print . runST) 的类型为 Show b => (forall s. ST s t) -> IO ()。 fourty_two 的类型为 ST x Int。

这里的 forall 是一种存在类型限定符 - 这意味着传递的参数必须是 通用的 在 s 上。也就是说，您必须传递一个多态类型，支持任何值的 s。如果您没有明确声明 forall，Haskell 将其放置在类型定义的最外层。这意味着 fourty_two :: forall x. ST x Int 和 (print . runST) :: forall t. Show t => (forall s. ST s t) -> IO ()

现在，我们可以通过让 t = Int, x = s 来将 forall x. ST x Int 与 forall s. ST s t 匹配。因此，直接调用的情况下是有效的。但如果我们使用 $ 呢？

$ 的类型为 ($) :: forall a b. (a -> b) -> a -> b。当我们解析 a 和 b 时，由于 $ 的类型没有任何显式的类型作用域，所以 fourty_two 的 x 参数被提升到了 ($) 类型的最外层作用域中 - 因此，($) :: forall x t. (a = forall s. ST s t -> b = IO ()) -> (a = ST x t) -> IO ()。此时，它尝试匹配 a 和 b，但失败了。

如果你改为写成((print . runST) $) fourty_two，那么编译器首先解析((print . runST $))的类型。它将($)的类型解析为forall t. (a = forall s. ST s t -> b = IO ()) -> a -> b；请注意，由于第二个a的出现是无约束的，因此我们没有让烦人的类型变量泄漏到最外层范围！因此匹配成功，函数被部分应用，表达式的整体类型为forall t. (forall s. ST s t) -> IO ()，这正好回到了我们开始的地方，所以它成功了。

- bdonlan

---

在倒数第二段，我不明白为什么 x 会被“提升”。x 不是编译器创建的实际类型吗？据我所知，它是一个隐藏的类型，我们永远无法访问它，但它就像 Int 一样。我们不需要提升 Int，为什么要提升 x？ - Clinton

“x” 实际上是编译器生成的实际类型“X12345”（尽管我们永远无法访问它），对吗？ - Clinton

@Clinton，x不是一种类型，它是一个类型变量。而且我不确定为什么它选择将fourty_two的隐式量化提升到外层的... $ ...表达式类型。然而你不能提升Int的量化，因为那不是一个类型变量，而是一种类型。 - bdonlan

好的，但是为什么s没有在（print . runST）中被提升？ - Clinton

可能是因为一开始就明确量化了吧？ - bdonlan

您可能对编辑后的问题特别感兴趣，尤其是主函数（5）。它显示中缀“.”有一些特殊的用法。 - Clinton