Haskell rank 2 多态性编译错误

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) 我已经阅读了以下两个问题（first、second），并且我被引导相信$ 只能用单态类型实例化。但我同样会假设 . 只能用单态类型实例化，因此同样会失败。 为什么第一个代码成功但第二个代码没有？ （例如，GHC 是否有针对第一种情况的特殊规则不能在第二种情况下适用？）

2) 当前是否有编译第二个代码的 GHC 扩展？ （也许ImpredicativePolymorphism 在某个时候这样做了，但它似乎已被弃用，有什么替代它的吗？）

3) 有没有办法使用 GHC 扩展来定义say `my_dollar` 来做 $ 所做的事情，但也能够处理多态类型，所以 (print . runST) `my_dollar` fourty_two 编译？

编辑：建议的答案：

另外，以下编译失败：

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

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

因此，GHC 似乎对$ 和. 都有特殊规则，但只有它们的中缀版本。

Answer 1

1. 我不确定我是否理解为什么第二个不起作用。我们可以查看print . runST 的类型并观察到它具有足够的多态性，因此责任不在于(.)。我怀疑 GHC 对中缀 ($) 的特殊规则还不够。如果您将此片段作为他们跟踪器上的错误提出，SPJ 和朋友可能会重新检查它。

   至于为什么第三个例子有效，那是因为((print . runST) $) 的类型又是足够多态的；其实就等于print . runST的类型。

2. 没有什么可以取代ImpredicativePolymorphism，因为GHC 人员还没有看到任何用例，其中额外的程序员便利性超过了编译器错误的额外可能性。 （我认为他们也不会认为这是有说服力的，尽管我当然不是权威。）

3. 我们可以定义一个稍微不那么多态的($$)：

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

   然后您的示例类型检查可以使用这个新运算符：

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

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 参数被提升到@ 类型的最外层范围987654342@ - 所以($) :: 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 ()，正好回到我们开始的地方，所以它成功了。