3

我决定简化我的代码,看看是什么条件产生了错误。我从一个简单的嵌套“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.在返回类型中提供 a 来指定它:

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

上面的示例确实在没有 final 的情况下编译,forall但是在我尝试调试的情况下这是不可能的。无论如何,在这种情况下,它可以编译任何一种方式。

我可以使用上面的代码将状态的多种用途链接在一起:

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

现在我尝试将 IO 加入其中,因此我使用了应用程序 fmap <$>。这不编译:(注意,如果我使用fmapor>>= 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

我从这个关于 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 操作进行交互。它对于单次迭代非常有效,但是我无法进一步使用返回值。

4

1 回答 1

0

我不确定所有这些在您的实际代码中是如何工作的,在我看来,您正在做的事情比严格必要的更复杂,但由于我不能说太多,所以我只会解决您的问题中的直接问题。

为什么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

我们在这里所做的只是引入了一个笨拙的替代 for letandwhere表达式。但这没有什么意义,因为lambda 参数必须具有完全实例化testFoofmap类型,所以我们无法注释掉我们的麻烦。

我们可以尝试以下方法:

{-# 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有 type ST s (Foo s)。但这也行不通,因为extractFoo需要一个forall量化的参数,并且sf是单态的。现在——如果你在 GHCi 中尝试这个版本——我们得到的错误信息不再是关于逃避 skolem,而是一个很好的老式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 extractGHCi 并显示浮动类型。

一个可能的解决方案是启用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'类型用于多个要包装的类型)。

于 2014-10-04T12:47:30.340 回答