runST - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Chris Wendt

It seems to me that the forall s existential quantifier in runST is the linchpin that enforces sequential reads/writes in the ST 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?

TheMatten

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

Peter Kjeld Andersen

I've been confused by how runST works this week actually. It throws an error when I try this in the repl:

λ> :type \m k -> runST $ m >>= k
<interactive>:1:23: error:
     Couldn't match expected type a0 -> ST s a with actual type p1
        because type variable s would escape its scope

And if I feed it a function (say initMV) for that m that returns ST s (MV.MVector s SomeUnboxType), it still complains:

λ> :type \k -> runST $ initMV >>= k

<interactive>:1:60: error:
     Couldn't match expected type MV.MVector s SomeUnboxType -> ST s a
                  with actual type p
        because type variable s would escape its scope

but if I replace the k with something a simple as V.freeze there are no problems at all:

λ> :type runST $ initMV  >>= V.freeze
runST $ initMV  >>= V.freeze :: V.Vector SomeUnboxType

what's GHC struggling with exactly?

TheMatten

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?

TheMatten

p1 "lives longer" than s, so unifying with it would be bad - try giving k binding as concrete annotation as possible (or use type signature)

TheMatten

(That is, something like forall s. something -> ST s somethingElse)

Peter Kjeld Andersen
λ> :type \(k :: forall s. MV.MVector s SomeUnboxType -> ST s somethingElse) -> runST $ initMV >>= k

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 of mv and k.

TheMatten

You could use typed holes instead of bindings:

λ> :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 even tells you what "fits" there

Chris Wendt

This seems close, but still isn't well-typed "Couldn't match type ‘s’ with ‘s0’":

x :: (forall s. (ST s a, a -> ST s ())) -> ()
x (m, k) = runST $ m >>= k
Chris Wendt

If that were well-typed, I think you could replace a with f s to support passing STRefs from m to k:

x :: (forall s. (ST s (f s), f s -> ST s ())) -> ()
x (m, k) = runST $ m >>= k
Chris Wendt

@Peter Kjeld Andersen I think I solved it with the help of @TheMatten

data F a s = F (STRef s a)
unF (F f) = f

y :: (forall s. (ST s (f s), (f s) -> ST s b)) -> b
y t = runST $ let (m, k) = t in m >>= k

useit = y (F <$> newSTRef 'c', readSTRef . unF)

Instead of F (STRef s a), you'd probably use something like Flip p a b, but it seems like this would be extremely cumbersome to use :oh_no: