I would say common explanation is that existential s prohibits you from using one STRef in multiple instances of runST - so you could try to run those ST actions in separate runSTs, but you wouldn't have any STRef to pass to them
It may be trying avoid unifying some external variable (I guess it infers k :: p1from lambda) with type that contains existential, because it's not sure whether it could be used outside of proper scope (runST) that way, thus "escaping"? But when you use freeze, it's type is filled in inside of runST call, so it should be fine?
But at that stage I guess you already know the structure of the types for your function and it's not as useful for getting to that point as λ> :type \mv k -> runST $ mv >>= k would have been if that could have told you some information about the types of mv and k.
λ> :t runST $ _mv >>= _k
<interactive>:1:9: error:
• Found hole: _mv :: ST s a0
Where: ‘a0’ is an ambiguous type variable
‘s’ is a rigid type variable bound by
a type expected by the context:
forall s. ST s a
at <interactive>:1:9-18
Or perhaps ‘_mv’ is mis-spelled, or not in scope
• In the first argument of ‘(>>=)’, namely ‘_mv’
In the second argument of ‘($)’, namely ‘_mv >>= _k’
In the expression: runST $ _mv >>= _k
<interactive>:1:17: error:
• Found hole: _k :: a0 -> ST s a
Where: ‘a0’ is an ambiguous type variable
‘s’ is a rigid type variable bound by
a type expected by the context:
forall s. ST s a
at <interactive>:1:9-18
‘a’ is a rigid type variable bound by
the inferred type of it :: a
at <interactive>:1:1
Or perhaps ‘_k’ is mis-spelled, or not in scope
• In the second argument of ‘(>>=)’, namely ‘_k’
In the second argument of ‘($)’, namely ‘_mv >>= _k’
In the expression: runST $ _mv >>= _k
• Valid hole fits include
fixST :: forall a s. (a -> ST s a) -> ST s a
with fixST @a @s
(imported from ‘Control.Monad.ST’
(and originally defined in ‘base-4.14.0.0:Control.Monad.ST.Imp’))
return :: forall (m :: * -> *) a. Monad m => a -> m a
with return @(ST s) @a
(imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))
fail :: forall (m :: * -> *) a. MonadFail m => String -> m a
with fail @(ST s) @a
(imported from ‘Prelude’
(and originally defined in ‘Control.Monad.Fail’))
pure :: forall (f :: * -> *) a. Applicative f => a -> f a
with pure @(ST s) @a
(imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))
id :: forall a. a -> a
with id @(ST s a)
(imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))
head :: forall a. [a] -> a
with head @(ST s a)
(imported from ‘Prelude’ (and originally defined in ‘GHC.List’))
(Some hole fits suppressed; use -fmax-valid-hole-fits=N or -fno-max-valid-hole-fits)
It seems to me that the
forall s
existential quantifier inrunST
is the linchpin that enforces sequential reads/writes in theST
monad, but I'd like to hear other people's take on it. I wrote a blog post about it https://chrismwendt.github.io/blog/2018/03/02/what-if-run-st-did-not-use-existential-quantification.html Is this a useful way to view it? Are there any glaring problems with looking at it this way?I would say common explanation is that existential
s
prohibits you from using oneSTRef
in multiple instances ofrunST
- so you could try to run thoseST
actions in separaterunST
s, but you wouldn't have anySTRef
to pass to themI've been confused by how
runST
works this week actually. It throws an error when I try this in the repl:And if I feed it a function (say
initMV
) for thatm
that returnsST s (MV.MVector s SomeUnboxType)
, it still complains:but if I replace the
k
with something a simple asV.freeze
there are no problems at all:what's GHC struggling with exactly?
It may be trying avoid unifying some external variable (I guess it infers
k :: p1
from lambda) with type that contains existential, because it's not sure whether it could be used outside of proper scope (runST
) that way, thus "escaping"? But when you usefreeze
, it's type is filled in inside ofrunST
call, so it should be fine?p1
"lives longer" thans
, so unifying with it would be bad - try givingk
binding as concrete annotation as possible (or use type signature)(That is, something like
forall s. something -> ST s somethingElse
)Yeah that works with
RankNTypes
on.But at that stage I guess you already know the structure of the types for your function and it's not as useful for getting to that point as
λ> :type \mv k -> runST $ mv >>= k
would have been if that could have told you some information about the types ofmv
andk
.You could use typed holes instead of bindings:
It even tells you what "fits" there
This seems close, but still isn't well-typed "Couldn't match type ‘s’ with ‘s0’":
If that were well-typed, I think you could replace
a
withf s
to support passingSTRef
s fromm
tok
:@Peter Kjeld Andersen I think I solved it with the help of @TheMatten
Instead of
F (STRef s a)
, you'd probably use something likeFlip p a b
, but it seems like this would be extremely cumbersome to use :oh_no: