为什么我不能为本地 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 块中，以便能够像这样使用在 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 与 run 中的 s 相同。

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

如果不打开语言扩展以允许您引用已经在范围内的 s 类型变量，就不可能为我的 read 或您的 loop 编写类型.使用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 实际上是指外部类型签名，而不是一个新的阴影类型变量。这就是您如何向类型系统承诺您只会在拥有它使用的 ref 的事务内部使用此 read 函数。

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

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

Why can't i give an explicit type signature to a local let bound ST action

haskell

existential-type

type-signature

type-variables

scoped-type-variables