如何在Either中收集ST动作列表?

rya*_*hza 6 haskell

如何将转换[Either ST]为a Either [ST]并随后依次运行操作?以下代码似乎适用于运行ST操作列表,但是当尝试在Either中生成操作列表(交换test下面的定义)时,类型不再排列.我本来期望列表的类型是相同的,所以我非常感谢对这些差异的任何解释.

{-# LANGUAGE RankNTypes #-}

import qualified Data.STRef as ST
import qualified Control.Monad.ST as ST

run :: (forall s. [ST.STRef s Int -> ST.ST s Int]) -> Int
run fs =
  ST.runST $ do
    x <- ST.newSTRef 0
    mapM_ (\f ->
        f x >>= ST.writeSTRef x
      ) fs
    ST.readSTRef x

action :: ST.STRef s Int -> ST.ST s Int
action = \x -> ST.readSTRef x >>= \y -> return (y + 1)

-- test :: Either String Int
-- test = mapM (const (return action)) [0..5] >>= \fs -> return (run fs)

test :: Int
test = run (map (const action) [0..5])

main = print test
Run Code Online (Sandbox Code Playgroud)

Rei*_*ton 10

存在更高级别类型的类型推断是不可判定的.GHC的类型推理算法做了一些简化的假设,这使得它不完整.其中包括:

  • GHC将假设由lambda绑定的变量是一个单一型(它不包含(领先?)foralls)

  • 当您使用多态函数时,GHC将假定其类型中的自由类型变量将在monotypes中实例化

如果您礼貌地要求GHC使用特定的多元型,则可以覆盖这两个假设.

现在,您如何期望您的程序键入检查?

  • 为了run fs打字检查,我们最好有fs :: forall s. [ST.STRef s Int -> ST.ST s Int]
  • 所以,根据上面的第一点,我们必须在绑定它的lambda上写下这种类型的签名:( \(fs :: forall s. [ST.STRef s Int -> ST.ST s Int]) -> ...使用ScopedTypeVariables)
  • 现在考虑使用>>=.它的类型是Monad m => m a -> (a -> m b) -> m b.但是,我们需要a = forall s. [ST.STRef s Int -> ST.ST s Int].所以,根据上面的第二点,我们需要给它>>=一个类型签名,如

    ... `op` (\(fs :: forall s. [ST.STRef s Int -> ST.ST s Int]) -> ...)
        where op :: Monad m
                 => m (forall s. [ST.STRef s Int -> ST.ST s Int])
                 -> ((forall s. [ST.STRef s Int -> ST.ST s Int]) -> m b)
                 -> m b
              op = (>>=)
    
    Run Code Online (Sandbox Code Playgroud)
  • 现在我们遇到了一个新问题.在这个应用程序中op,第一个参数有类型Either String (forall s. [ST.STRef s Int -> ST.ST s Int]).(->)除非您打开(损坏的)ImpredicativeTypes,否则不允许将类型构造函数(除了)应用于多边形类型.但是,我们可以打开并继续......
  • 潜入第一个参数,我们可以看到我们需要return :: Monad m => a -> m a实例化a = forall s. ST.STRef s Int -> ST.ST s Int.因此,我们需要添加另一种类型的签名return
  • 同样,我们需要mapM :: Monad m => (a -> m b) -> [a] -> m [b]实例化b = forall s. ST.STRef s Int -> ST.ST s Int
  • 如果你正在密切关注,你会发现另一个问题:mapMhas类型的结果

    Either String [forall s. ST.STRef s Int -> ST.ST s Int]
    
    Run Code Online (Sandbox Code Playgroud)

    但是论证(>>=)需要是类型的

    Either String (forall s. [ST.STRef s Int -> ST.ST s Int])
    
    Run Code Online (Sandbox Code Playgroud)

    你需要在这些之间进行转换.实际上这是一个无操作,但GHC并不够聪明,所以你必须进行线性时间转换,比如

    liftM (\x -> map (\(y :: forall s. ST.STRef s Int -> ST.ST s Int) -> y) x)
    
    Run Code Online (Sandbox Code Playgroud)

    (除了liftM需要另一种类型的签名)

故事的道德:你可以这样做,但你不应该这样做.

如果你把你的foralls 隐藏在像new这样的新类型中,你通常会有一个更容易的时间

newtype S s = S { unS :: forall s. ST.STRef s Int -> ST.ST s Int }
Run Code Online (Sandbox Code Playgroud)

这使得在程序中引入多态性的点更加明确(通过出现SunS).


sha*_*ang 6

您需要将函数包装在一个中newtype以保留存在量化,而不必使用ImpredicativeTypes.

{-# LANGUAGE RankNTypes #-}

import qualified Data.STRef as ST
import qualified Control.Monad.ST as ST

newtype STFunc = STFunc (forall s. ST.STRef s Int -> ST.ST s Int)

run :: [STFunc] -> Int
run fs = ST.runST $ do
    x <- ST.newSTRef 0
    mapM_ (\(STFunc f) ->
        f x >>= ST.writeSTRef x
      ) fs
    ST.readSTRef x

action :: STFunc
action = STFunc $ \x -> ST.readSTRef x >>= \y -> return (y + 1)

test :: Either String Int
test = mapM (const (return action)) [0..5] >>= \fs -> return (run fs)

main = print test
Run Code Online (Sandbox Code Playgroud)