为什么我不能为本地 let 绑定 ST 操作提供显式类型签名

Question

我有以下运行良好的简化程序：

\n

{-# LANGUAGE Rank2Types #-}\nmodule Temp where\n\nimport Control.Monad.ST\nimport Control.Monad\nimport Data.STRef\n\nmystery :: Int -> Int\nmystery start =\n  let\n    run :: ST s Int\n    run = do\n      count <- newSTRef (1::Int)\n      loop count start\n      readSTRef count\n  in\n    runST run\n\nloop :: STRef s Int -> Int -> ST s ()\nloop cnt n = when (n /= 1) \n                  (modifySTRef cnt succ >> \n                     if n `mod` 2 == 0 \n                       then  loop cnt (n `div` 2) \n                       else  loop cnt (n * 3 + 1))\n

\n

我将loop定义移动到块内do，以便能够使用创建的计数器，如下run所示：

\n

mystery :: Int -> Int\nmystery start =\n  let\n    run :: ST s Int\n    run = do\n      count <- newSTRef (1::Int)\n      let\n        loop :: Int -> ST s ()\n        loop n = when (n /= 1) \n                      (modifySTRef count succ >> \n                        if n `mod` 2 == 0 \n                          then  loop (n `div` 2) \n                          else  loop (n * 3 + 1))\n      loop start\n      readSTRef count\n  in\n    runST run\n

\n

这给了我以下错误：

\n

Couldn\'t match type \xe2\x80\x98s1\xe2\x80\x99 with \xe2\x80\x98s\xe2\x80\x99\n    \xe2\x80\x98s1\xe2\x80\x99 is a rigid type variable bound by\n      the type signature for:\n        loop :: forall s1. Int -> ST s1 ()\n      at ...\n    \xe2\x80\x98s\xe2\x80\x99 is a rigid type variable bound by\n      the type signature for:\n        run :: forall s. ST s Int\n      at ...\n    Expected type: ST s1 ()\n    Actual type: ST s ()\n    In the expression:\n     ...\n

\n

我知道这s是不允许逃脱的，但据我所知它不会？此外，当我删除类型签名时，loop问题就消失了。我想这表明\n他们的签名在某种程度上是不正确的，但它与以前相同，除了没有计数器，而且我不知道它应该是什么。

\n

重命名s以匹配或不匹配s中提到的run没有什么区别。

\n

Answer 1

首先，让我们重命名类型变量，以便更容易讨论，并删除与此错误无关的程序部分：

mystery :: Int
mystery = runST run
  where run :: ST s Int
        run = do
          ref <- newSTRef 1
          let read :: ST t Int
              read = readSTRef ref
          read

这表现出相同的行为，并像以前一样注释掉类型签名来read修复它。

现在，我们问： 的类型是什么ref？newSTRefis的类型a -> ST s (STRef s a)，因此ref :: STRef s Int，where与ins相同。srun

的类型是什么readSTRef ref？出色地，readSTRef :: STRef s a -> ST s a。因此，readSTRef ref :: ST s Int，其中 s 又是 的定义中的那个run。您给它一个类型签名，声称它适用于 any t，但它仅适用于特定的sin run，因为它使用来自该事务的引用。

如果不打开语言扩展来允许您引用已经在范围内的类型变量，就不可能为 myread或 your编写类型。使用，您可以编写：loopsScopedTypeVariables

{-# LANGUAGE ScopedTypeVariables #-}

import Control.Monad.ST
import Data.STRef

mystery :: Int
mystery = runST run
  where run :: forall s. ST s Int
        run = do
          ref <- newSTRef 1
          let read :: ST s Int
              read = readSTRef ref
          read

forall显式使用“s进入范围”，以便您可以引用它。现在，内部类型签名s实际上引用了外部类型签名，而不是一个新的影子类型变量。这就是您向类型系统承诺的方式：您只会read在拥有它所使用的引用的事务内部使用此函数。

您的原始程序（具有顶级 ）也loop出于类似的原因而工作。它不是捕获 an STRef（因此它是隐式的），而是声明一个类型，该类型对引用和事务都s使用相同的类型。s它适用于任何交易，只要它从该交易中获得引用即可。