56

为什么这个类型检查：

runST $ return $ True

虽然以下没有：

runST . return $ True

GHCI 抱怨：

Couldn't match expected type `forall s. ST s c0'
            with actual type `m0 a0'
Expected type: a0 -> forall s. ST s c0
  Actual type: a0 -> m0 a0
In the second argument of `(.)', namely `return'
In the expression: runST . return
4

3 回答 3

52

简短的回答是类型推断并不总是适用于更高级别的类型。在这种情况下，它无法推断 的类型(.)，但它会检查我们是否添加了显式类型注释：

> :m + Control.Monad.ST
> :set -XRankNTypes
> :t (((.) :: ((forall s0. ST s0 a) -> a) -> (a -> forall s1. ST s1 a) -> a -> a) runST return) $ True
(((.) :: ((forall s0. ST s0 a) -> a) -> (a -> forall s1. ST s1 a) -> a -> a) runST return) $ True :: Bool

如果我们($)用我们自己的版本替换，您的第一个示例也会出现同样的问题：

> let app f x = f x
> :t runST `app` (return `app` True)
<interactive>:1:14:
    Couldn't match expected type `forall s. ST s t0'
                with actual type `m0 t10'
    Expected type: t10 -> forall s. ST s t0
      Actual type: t10 -> m0 t10
    In the first argument of `app', namely `return'
    In the second argument of `app', namely `(return `app` True)'

同样，这可以通过添加类型注释来解决：

> :t (app :: ((forall s0. ST s0 a) -> a) -> (forall s1. ST s1 a) -> a) runST (return `app` True)
(app :: ((forall s0. ST s0 a) -> a) -> (forall s1. ST s1 a) -> a) runST (return `app` True) :: Bool

这里发生的是 GHC 7 中有一个特殊的类型规则，它只适用于标准($)运算符。Simon Peyton-Jones在 GHC 用户邮件列表的回复中解释了这种行为：

这是可以处理禁言类型的类型推断的一个激励示例。考虑以下类型($)：

($) :: forall p q. (p -> q) -> p -> q

在这个例子中，我们需要用 来实例化p，(forall s. ST s a)这就是暗示多态性的意思：用多态类型实例化一个类型变量。

可悲的是，我知道没有一个合理复杂的系统可以在没有帮助的情况下对 [this] 进行类型检查。有很多复杂的系统，我是至少两篇论文的合著者，但它们都太复杂了，无法生活在 GHC 中。我们确实有一个 boxy 类型的实现，但是我在实现新的类型检查器时把它拿出来了。没有人理解它。

然而，人们经常写

runST $ do ...

在 GHC 7 中，我实现了一个特殊的类型规则，仅用于($). 只需将其(f $ x)视为一种新的句法形式，具有明显的打字规则，然后就可以了。

你的第二个例子失败了，因为没有这样的规则(.)。

于 2012-02-27T18:09:23.027 回答
36

这种runST $ do { ... }模式很常见，而且它通常不会进行类型检查的事实很烦人，以至于 GHC 包含了一些ST特定的类型检查技巧来使其工作。那些黑客可能会在这里为($)版本开火，但不是(.)版本。

于 2012-02-27T17:57:13.907 回答
3

这些消息有点令人困惑（或者我觉得）。让我重写你的代码：

runST (return True)   -- return True is ST s Bool
(runST . return) True  -- cannot work

另一种说法是单态m0 a0（返回的结果，如果它会得到a0）不能与（forall s.ST sa）统一。

于 2012-02-27T18:02:31.653 回答