问题描述
为什么要进行类型检查:
Why does this typecheck:
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
推荐答案
简短的回答是类型推断并不总是适用于更高级别的类型.在这种情况下，它无法推断 (.) 的类型，但它会检查我们是否添加了显式类型注释:
The short answer is that type inference doesn't always work with higher-rank types. In this case, it is unable to infer the type of (.), but it type checks if we add an explicit type annotation:
> :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
同样的问题也发生在你的第一个例子中，如果我们用我们自己的版本替换 ($):
The same problem also happens with your first example, if we replace ($) with our own version:
> 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)'
同样，这可以通过添加类型注释来解决:
Again, this can be solved by adding type annotations:
> :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 用户邮件列表的回复中解释了这种行为一个>:
What is happening here is that there is a special typing rule in GHC 7 which only applies to the standard ($) operator. Simon Peyton-Jones explains this behavior in a reply on the GHC users mailing list:
这是一个可以处理类型推断的激励示例非谓语类型.考虑($)的类型:
($) :: forall p q. (p -> q) -> p -> q
在例子中我们需要用(forall s.ST s a)来实例化p，这就是不可预测的多态性意味着:用一个多态类型.
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.
遗憾的是，我知道没有合理复杂性的系统可以进行类型检查[这个] 没有帮助.有很多复杂的系统，我有是至少两篇论文的合著者，但他们都太Jolly 生活在 GHC 中很复杂.我们确实有一个实现四四方方的类型，但我在实现新的类型检查器时将其取出.没有人理解它.
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.
然而，人们经常写作
runST $ do ...
在 GHC 7 中，我实现了一个特殊的类型规则，仅用于 ($) 的中缀使用.把 (f $ x) 想象成一个新的句法形式，带有明显的打字规则，然后就可以了.
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.
你的第二个例子失败了，因为 (.) 没有这样的规则.
Your second example fails because there is no such rule for (.).
这篇关于runST 和函数组合的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！