Mixing IO w / ST Monad - "variable of type s2" would disappear due to its volume "

I decided to simplify my code to find out what conditions caused the error. I start with a simple nested "s" like ST s (STArray s x y)

this:

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

data Foo s = Foo { foo::Bool }

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

      

To check the status code, I run the following transformation:

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

      

I would like to extract the value from the state while saving the state, so the next step would be to extract the Bool value:

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)

      

To extract this Bool, I have to use runST

. I understand that this will create additional state, which I will provide by providing forall s.

in the return type:

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

      

The example above compiles without final forall

, however in the circumstance I am trying to debug this is not possible. Regardless, in this case, it compiles anyway.

I can use the above code to combine multiple uses of state together:

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

      

Now I am trying to throw IO into the mix and so I am using applicative fmap <$>

. This won't compile: (NB. Same problem if I use fmap

or >>= return

rather than <$>

)

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

      

With the following error:

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

      

I know from this SO question about the structure of ST functions that not all possible uses of ST are taken into account by the compiler. To test this assumption, I modified the above function to not use IO and just pass the return value to the 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

      

Predictably this also fails to compile with an identical error message.

It's a challenge. I have a reasonable amount of I / O that needs to interact with a set of deeply nested ST operations. It works fine for one iteration, however I cannot use the return value anymore.

+3


source to share


1 answer


I'm not sure how this all works in your real code and it seems to me that you are doing something more convoluted than strictly necessary, but since I cannot say much definitively about this, I will only refer to the nearest problems in your question.

Why testBar

doesn't it work

In (\(b,sf) -> extractFoo $ splitChangeFoo sf) <$> testBar'

we have <$>

, which has a type forall a b. (a -> b) -> IO a -> IO b

. However, it testBar

has a type forall s. IO (Bool, ST s (Foo s))

. We can only apply fmap

to testBar

after s

.

In your case s

, a new variable is instantiated s0

, so inside the lambda sf

there is this parameter as well. Unfortunately, it s0

differs from the topmost parameter s

(which we would like to see in the return type), so it sf

is currently practically not used.

In case the testFooBar

problem is that the lambda arguments are monomorphic by default (otherwise type inference would become undecidable), so we just need to annotate the type:

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

      

All we have done here is introduce a cumbersome alternative for expressions let

and where

. But that doesn't matter as testFoo

fmap

it requires the lambda argument to be fully instance type, so we can't annotate our troubles.

We can try the following:

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

      

Now testBar

has the correct s

parameter; since it is no longer generalized, we can immediately apply to it fmap

. Internally, the lambda sf

has a type ST s (Foo s)

. But this also won't work, since a extractFoo

expects a forall

quantitative argument, but sf

is monomorphic. Now - if you try this version in GHCi - the error message we get is no longer related to skolems speedup, but good old fashioned one can't match type s with s2

.

How to help

Obviously extract

must return forall s.

-ed in some way ST s (Foo s)

. Your original type doesn't fit because GHC doesn't have polymorphic return types, so



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

      

actually means

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

      

since GHC pops up all forall

-s at the top of the area. This simplifies type inference and allows the use of typecheck terms. Indeed, you can type :t extract

in GHCi and represent it as a float.

A possible solution would include ImprediactiveTypes

and have

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

      

But there is a reason why it is ImpredicativeTypes

rarely used: it is poorly integrated with the rest of the type checking machine and tends to fail for all but the simplest purposes. As an example, assuming extract

with a changed type, the following example does not check the type:

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

      

But it changes the typecheck when we change (\(b, sf) -> (b, sf))

to (\x -> x)

! So let's forget about the troubled types.

The usual solution is to just wrap quantitative types in newtype. It's much less flexible than the non-specific type, but at least it works.

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

      

So, whenever you need to return quantitative types, wrap it in a new type and then expand as needed. You might want to stick with the normal type argument scheme for your custom types (for example, always make the parameter s

last, so you can use the same type ST'

for multiple types to be wrapped).

0


source







All Articles