How can I collect a list of ST actions inside Either?

Question

How can I go about converting an [Either ST] to an Either [ST] and subsequently run the actions sequentially? The below code appears to work for running a list of ST actions, however when trying to generate the list of actions in Either (swapping the test definitions below) the types no longer line up. I would have expected the types of the lists to be identical so I would greatly appreciate any explanation of the differences.

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

Answer 1

Type inference in the presence of higher-rank types is undecidable. GHC's type inference algorithm makes some simplifying assumptions, which render it incomplete. Those include:

• GHC will assume the variable bound by a lambda is a monotype (it does not contain (leading?) foralls)

• When you use a polymorphic function, GHC will assume that the free type variables in its type will be instantiated at monotypes

Both of these assumptions can be overridden if you ask GHC politely to use a particular polytype instead.

Now, how do you expect your program to type check?

• In order for run fs to type check, we had better have fs :: forall s. [ST.STRef s Int -> ST.ST s Int]
• So, according to the first point above we must write this type signature on the lambda that binds it: \(fs :: forall s. [ST.STRef s Int -> ST.ST s Int]) -> ... (using ScopedTypeVariables)

• Now consider the use of >>=. Its type is Monad m => m a -> (a -> m b) -> m b. But, we need a = forall s. [ST.STRef s Int -> ST.ST s Int]. So, according to the second point above we need to give this >>= a type signature, as in

  ... `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 = (>>=)
  

• Now we run into a new kind of problem. In this application of op, the first argument has type Either String (forall s. [ST.STRef s Int -> ST.ST s Int]). Application of a type constructor (other than (->)) to a polytype is not allowed, unless you turn on the (broken) ImpredicativeTypes. However, we can turn it on and continue...
• Diving into the first argument, we can see that we will need return :: Monad m => a -> m a instantiated at a = forall s. ST.STRef s Int -> ST.ST s Int. So, we need to add another type signature to return
• Similarly we will need mapM :: Monad m => (a -> m b) -> [a] -> m [b] instantiated at b = forall s. ST.STRef s Int -> ST.ST s Int

• If you are paying close attention you will notice yet another problem: the result of the mapM has type

  Either String [forall s. ST.STRef s Int -> ST.ST s Int]
  

  but the argument of (>>=) needs to be of type

  Either String (forall s. [ST.STRef s Int -> ST.ST s Int])
  

  and you will need to convert between these. In reality this is a no-op, but GHC is not smart enough to know it, so you will have to do a linear-time conversion, something like

  liftM (\x -> map (\(y :: forall s. ST.STRef s Int -> ST.ST s Int) -> y) x)
  

  (except liftM will need yet another type signature)

Moral of the story: You can do this, but you shouldn't.

You will generally have an easier time if you hide your foralls inside newtypes like

newtype S s = S { unS :: forall s. ST.STRef s Int -> ST.ST s Int }

which makes the points where polymorphism is introduced more explicit in your program (via occurrences of S and unS).