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

Question

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

{-# LANGUAGE Rank2Types #-}
module Temp where

import Control.Monad.ST
import Control.Monad
import Data.STRef

mystery :: Int -> Int
mystery start =
  let
    run :: ST s Int
    run = do
      count <- newSTRef (1::Int)
      loop count start
      readSTRef count
  in
    runST run

loop :: STRef s Int -> Int -> ST s ()
loop cnt n = when (n /= 1) 
                  (modifySTRef cnt succ >> 
                     if n `mod` 2 == 0 
                       then  loop cnt (n `div` 2) 
                       else  loop cnt (n * 3 + 1))

我将 loop 定义移动到 do block 中，以便能够像这样使用在 run 中创建的计数器:

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

这给了我以下错误:

Couldn't match type ‘s1’ with ‘s’
    ‘s1’ is a rigid type variable bound by
      the type signature for:
        loop :: forall s1. Int -> ST s1 ()
      at ...
    ‘s’ is a rigid type variable bound by
      the type signature for:
        run :: forall s. ST s Int
      at ...
    Expected type: ST s1 ()
    Actual type: ST s ()
    In the expression:
     ...

我知道 s 不允许转义，但据我所知，它不会转义？此外，当我删除 loop 的类型签名时，问题就消失了。我想这表明他们的签名不知何故不正确，但它和以前一样，只是没有计数器，我不知道它应该是什么。

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

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 的类型是什么？ ？ newSTRef 的类型是 a -> ST s (STRef s a) , 所以 ref :: STRef s Int , 其中s与 s 相同在 run .

readSTRef ref 的类型是什么？ ？嗯， readSTRef :: STRef s a -> ST s a .所以，readSTRef ref :: ST s Int , 其中 s 又是 run 定义中的那个 。你给它一个类型签名，声称它适用于任何 t , 但它只适用于特定的 s在 run ，因为它使用了该交易的引用。

不可能为我的read写类型或者你的 loop无需打开语言扩展即可让您引用 s已经在范围内的类型变量。与 ScopedTypeVariables ，你可以这样写:

{-# 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从拥有它使用的 ref 的事务内部运行。

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