ST Trick with existentials types/rigid skolem

ST Trick

newtype ST s a = ST { unsafeRunST :: a } -- phantom type s

instance Functor (ST s) where
  fmap f (ST a) = seq a (ST $ f a)

instance Applicative (ST s) where
  pure = ST
  ST f <*> ST a = seq f . seq a $ (ST $ f a)

instance Monad (ST s) where
  ST a >>= f = seq a $ f a

newtype STRef s a = STRef { unSTRef :: IORef a } -- s phantom type

newSTRef :: a -> ST s (STRef s a) -- same 's' <- irrevocable linking between the types.
newSTRef = pure . STRef . unsafePerformIO . newIORef

readSTRef :: STRef s a -> ST s a
readSTRef = pure . unsafePerformIO . readIORef . unSTRef

writeSTRef :: STRef s a -> a -> ST s ()
writeSTRef ref = pure . unsafePerformIO . writeIORef (unSTRef ref)

modifySTRef :: STRef s a -> (a -> a) -> ST s ()
modifySTRef ref f = do
  a <- readSTRef ref
  writeSTRef ref $ f a

runST :: forall a. (forall s. ST s a) -> a
runST = unsafeRunST

If you try to run this, it won't compile

>>> runST (newSTRef True) -- Compilation error

It is really easy to see if you specialize the types of runST @STRef s a:

runST :: (forall s. ST s (STRef s Bool)) -> STRef s Bool

The type variable s only exists inside the quantifier for all. "s" can't scape the quantifier scope, so "s" does not exists outside it!

monadplus/st.md

ST Trick