haskell - runST和函数组成

Question

为什么要进行类型检查:

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

Answer 1

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

> :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 在 a reply on the GHC users mailing list 中解释了这种行为:

This is a motivating example for type inference that can deal with impredicative types. Consider the type of ($):

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

In the example we need to instantiate p with (forall s. ST s a), and that's what impredicative polymorphism means: instantiating a type variable with a polymorphic type.

Sadly, I know of no system of reasonable complexity that can typecheck [this] unaided. There are plenty of complicated systems, and I have been a co-author on papers on at least two, but they are all Too Jolly Complicated to live in GHC. We did have an implementation of boxy types, but I took it out when implementing the new typechecker. Nobody understood it.

However, people so often write

runST $ do ... 

that in GHC 7 I implemented a special typing rule, just for infix uses of ($). Just think of (f $ x) as a new syntactic form, with the obvious typing rule, and away you go.

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