混合 IO 带 ST Monad - "type variable `s2' would escape its scope"

Question

我决定简化代码，看看是什么条件导致了错误。我从一个类似于ST s (STArray s x y)的简单嵌套"s"开始，如下所示：

{-# 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 srcTests.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

我从这个关于ST函数组合的SO问题中了解到，并不是所有可能的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))。只有在s被实例化之后，我们才能将fmap应用到testBar。

在您的例子中，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.的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将所有CCD_ 41-s浮到作用域的顶部。这使得类型推断更容易，并允许更多的术语进行类型检查。事实上，您可以在GHCi中输入:t extract，并显示为浮点类型。

一个可能的解决方案是启用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)时，它确实进行了类型检查！所以，让我们忘记那些不明确的类型。

通常的解决方案是将量化的类型封装在一个新类型中。这远不如非专用类型灵活，但至少它能工作。

{-# 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'类型）。