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.
source to share
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).
source to share