haskell - 使用 ST Monad 混合 IO - "type variable ` s 2' would escape its scope"

Question

我决定简化我的代码，看看是什么条件产生了错误。我从一个简单的嵌套“s”开始，类似于 ST s (STArray s x y)像这样:

{-# LANGUAGE RankNTypes #-}
import Control.Monad.ST
import Control.Applicative

data Foo s = Foo { foo::Bool }

newFoo :: ST s (Foo s)
newFoo = return $ Foo False

为了测试状态代码，我运行以下转换:

changeFoo :: (forall s. ST s (Foo s)) -> ST s (Foo s)
changeFoo sf = do
   f <- sf
   let f' = Foo (not $ foo f)
   return f'

我想在保留状态的同时从状态中提取一个值，因此下一步是提取 Bool 值:

splitChangeFoo :: (forall s. ST s (Foo s)) -> ST s (Bool,(Foo s))
splitChangeFoo sf = do
   f <- changeFoo sf
   let b = foo f
   return (b,f)

为了提取该 Bool，我必须使用 runST 。我的理解是，这将创建一个附加状态，我通过提供 forall s. 来指定该状态。在返回类型中:

extractFoo :: (forall s. ST s (Bool,(Foo s))) -> (forall s. (Bool,ST s ((Foo s))))
extractFoo sbf = (runST $ fst <$> sbf,snd <$> sbf)

上面的示例在没有最终 forall 的情况下进行编译但是在我尝试调试的情况下这是不可能的。无论如何，在这种情况下它都会以任何一种方式编译。

我能够使用上面的代码将状态的多个使用链接在一起:

testFoo :: (Bool, ST s (Foo s))
testFoo = (b && b',sf')
   where
      (b,sf) = extractFoo $ splitChangeFoo newFoo
      (b',sf') = extractFoo $ splitChangeFoo sf

现在我尝试将 IO 加入其中，因此我使用了应用 fmap <$> 。这不会编译:(注意，如果我使用 fmap 或 >>= return 而不是 <$> 也会出现同样的问题)

testBar :: IO (Bool, ST s (Foo s))
testBar = (\(b,sf) -> extractFoo $ splitChangeFoo sf) <$> testBar'
   where
      testBar' :: IO (Bool, ST s (Foo s))
      testBar' = return $ extractFoo $ splitChangeFoo newFoo

出现以下错误:

Couldn't match type `s0' with `s2'
  because type variable `s2' would escape its scope
This (rigid, skolem) type variable is bound by
  a type expected by the context: ST s2 (Foo s2)
The following variables have types that mention s0
  sf :: ST s0 (Foo s0) (bound at src\Tests.hs:132:16)
Expected type: ST s2 (Foo s2)
  Actual type: ST s0 (Foo s0)
In the first argument of `splitChangeFoo', namely `sf'
In the second argument of `($)', namely `splitChangeFoo sf'
In the expression: extractFoo $ splitChangeFoo sf

我从这个SO question about ST function composition知道编译器并未考虑 ST 的所有可能用途。为了测试这个假设，我修改了上面的函数，不使用 IO，而是简单地将返回值传递给 lambda:

testFooBar :: (Bool, ST s (Foo s))
testFooBar = (\(b,sf) -> extractFoo $ splitChangeFoo sf) testFooBar'
   where
      testFooBar' :: (Bool, ST s (Foo s))
      testFooBar' = extractFoo $ splitChangeFoo newFoo

可以预见的是，这也不会在编译时出现相同的错误消息。

这提出了挑战。我有相当数量的 IO 需要与一组深度嵌套的 ST 操作进行交互。它对于单次迭代来说工作得非常好，但是我无法进一步使用返回值。

Answer 1

我不确定所有这些在你的实际代码中是如何实现的，在我看来，你正在做一些比严格必要的更复杂的事情，但由于我不能对此说太多明确的话，我会仅解决您问题中的直接问题。

为什么 testBar不起作用

在 (\(b,sf) -> extractFoo $ splitChangeFoo sf) <$> testBar' ，我们有<$> ，其类型为 forall a b. (a -> b) -> IO a -> IO b 。然而，testBar类型为forall s. IO (Bool, ST s (Foo s)) 。我们只能申请fmap至testBar s之后已经实例化了。

就您而言，s被实例化为一个新变量 s0 ，所以在 lambda sf 内也有这个参数。不幸的是，s0与最上面的 s 不同参数(我们希望在返回类型中看到)，所以 sf现在几乎无法使用。

以testFooBar为例，问题是 lambda 参数默认是单态的(否则类型推断将变得不可判定)，因此我们只需注释类型即可:

testFooBar :: (Bool, ST s (Foo s))
testFooBar =
  (\(x :: forall s. (Bool, (ST s (Foo s)))) -> extractFoo $ splitChangeFoo $ snd x) testFooBar'
   where
      testFooBar' :: (Bool, ST s (Foo s))
      testFooBar' = extractFoo $ splitChangeFoo newFoo

我们在这里所做的只是为 let 引入一个笨拙的替代方案。和where表达式。但这没有什么意义，因为在testFoo中fmap要求 lambda 参数具有完全实例化的类型，因此我们无法通过注释消除我们的问题。

我们可以尝试以下方法:

{-# LANGUAGE ScopedTypeVariables #-}

testBar :: forall s. IO (Bool, ST s (Foo s))
testBar = (\(b,sf) -> extractFoo $ splitChangeFoo sf) <$> testBar'
   where
      testBar' :: IO (Bool, ST s (Foo s))
      testBar' = return $ extractFoo $ splitChangeFoo newFoo

现在testBar有权利 s参数开头；由于它不再通用，我们可以应用fmap马上到它。在 lambda 内部，sf类型为ST s (Foo s) 。但这也行不通，因为 extractFoo预计 forall量化参数，和 sf是单态的。现在 - 如果你在 GHCi 中尝试这个版本 - 我们收到的错误消息不再是关于转义 skolems，而是一个很好的老式 can't match type s with s2 。

如何帮助它

显然，extract必须返回 forall s. -ed ST s (Foo s)不知何故。你的原始类型不好，因为 GHC 没有多态返回类型，所以

(forall s. ST s (Bool, Foo s)) -> (forall s. (Bool, ST s (Foo s)))

实际上意味着

forall s. (forall s. ST s (Bool, Foo s)) -> (Bool, ST s (Foo s))

自从 GHC 浮出所有 forall -s 到范围的顶部。这使得类型推断更加容易，并允许更多术语进行类型检查。事实上，您可以输入 :t extract在 GHCi 中并以浮出类型呈现。

一个可能的解决方案是启用 ImprediactiveTypes并拥有

extract :: (forall s. ST s (Bool, Foo s)) -> (Bool, forall s. ST s (Foo s))

但是 ImpredicativeTypes 是有原因的很少使用:它与类型检查机制的其余部分集成得很差，并且除了最简单的目的之外，很容易失败。例如，假设 extract使用修改后的类型，以下示例不会进行类型检查:

testBar :: IO (Bool, forall s. ST s (Foo s))
testBar = (\(b, sf) -> (b, sf)) <$> testBar'
  where
    testBar' :: IO (Bool, forall s. ST s (Foo s))
    testBar' = return $ extractFoo $ splitChangeFoo newFoo

但是当我们改变 (\(b, sf) -> (b, sf)) 时它会进行类型检查至(\x -> x) !所以让我们忘记命令式类型。

通常的解决方案是将量化类型包装在新类型中。这比命令式类型的灵 active 要差很多，但至少它是有效的。

{-# LANGUAGE RankNTypes #-}

import Control.Monad.ST
import Control.Applicative
import Control.Arrow

data Foo s = Foo { foo::Bool }
newtype ST' f = ST' {unST' :: forall s. ST s (f s)}

newFoo :: ST s (Foo s)
newFoo = return $ Foo False

splitChangeFoo :: ST s (Foo s) -> ST s (Bool, Foo s)
splitChangeFoo = fmap (\(Foo b) -> (b, Foo (not b)))

extract :: (forall s. ST s (Bool, Foo s)) -> (Bool, ST' Foo)
extract s = (runST $ fst <$> s, ST' $ snd <$> s)

testBar :: IO (Bool, ST s (Foo s))
testBar = (\(_, ST' s) -> second unST' $ extract $ splitChangeFoo s) <$>
          (return $ extract $ splitChangeFoo newFoo)

因此，每当您需要返回量化类型时，请将其包装在新类型中，然后根据需要展开。您可能希望为自定义类型坚持通用类型参数方案(例如，始终将 s 参数放在最后，这样您就可以将单个 ST' 类型用于多个要包装的类型)。