can you use polysemy with ST-like "thread" types?

[MaciekFlis]

I have this type from GPipe library: ContextT Handle os IO a where os is this "thread" type that limits the scope of what's inside ContextT, much like with ST monad
and I have a function runContextT :: (forall os. ContextT Handle os IO x) -> IO x
I'd like to be able to use use this with polysemy so I can mix other effects inside ContexT
currently I my effects are run in IO and then I liftIO to ContextT, but I'd like it to be a bit more streamlined (and testable).
So I wanted to make ContextT be basically the last effect on my stack to be interpreted IO, I tried wrapping this with my own type and interpreting it:

data GPipeWrapped os m a where
   GP :: (ContextT Handle os IO a) -> GPipeWrapped os m a
gp a = Polysemy.Internal.send (GP a)

and then interpreting:

runGPipeWrapped :: forall r os a. Member (Embed IO) r
                => Sem (GPipeWrapped os ': r) a
                -> Sem r a
runGPipeWrapped = interpret $ \case
  GP (x :: ContextT GLFW.Handle os IO x) ->
      embed $ runContextT GLFW.defaultHandleConfig x

I'm getting Could not deduce: os1 ~ os, so look's like I'm missing some RankN forall qualifier somewhere? I'm not even sure what I'm trying is possible in principle, any ideas?

[googleson78]

If your approach did work (note my use of unsafeCoerce), it would allow the s to escape (using ST because it's simpler):

module ST where

import Control.Monad.ST (runST, ST)
import Polysemy (Sem, Member, run, interpret)
import Polysemy.Internal (send)
import Unsafe.Coerce (unsafeCoerce)
import Data.STRef (newSTRef, STRef)

data STE s m a where
   STE :: ST s a -> STE s m a

ste :: Member (STE s) r => STE s (Sem r) a -> Sem r a
ste = send

runSTE ::
  forall r s a.
  Sem (STE s ': r) a ->
  Sem r a
runSTE = interpret $ \case
  STE x -> pure $ runST $ unsafeCoerce x

whoops :: forall s. STRef s Integer
whoops = run $ runSTE @_ @s ref

ref :: forall s r. Member (STE s) r => Sem r (STRef s Integer)
ref = ste $ STE $ newSTRef 42

I'm not sure what needs to be different to fill your use case.

[MaciekFlis]

This is a good analogue of what I want, thanks! Could there be another approach that works?
Does it mean that I would need a variant of Sem, like SemST that could thread the s type until runST? I'd like to keep the scope restriction, but also to compose this with other effects without leaving the scope.

[googleson78]

I think so, because you would be able to pass your "s-bound" values to other effects within the Sem, so your entire Sem should have the s threaded, so as to not leak it.

In other words, the same problem that you get (afaik) from trying to thread the s through other things (e.g. transformers).

Not sure how viable this would be for polysemy, but maybe some of the other "wizards" around here can think of something that magically solves this issue without a big rewrite for polysemy.

[TheMatten]

Seems doable once you look at ST as State (using STT transformer in place of StateT), and decouple effect datatype from the transformer:

#!/usr/bin/env stack
-- stack repl --package polysemy --package polysemy-plugin --package STMonadTrans

{-# options_ghc -fplugin=Polysemy.Plugin #-}
{-# language TemplateHaskell, BlockArguments, RankNTypes, LambdaCase, TypeApplications, ScopedTypeVariables, TypeOperators, GADTs, DataKinds, PolyKinds, FlexibleContexts, MagicHash #-}

module PolysemyST where

import GHC.Exts (State#)
import qualified Control.Monad.ST.Trans as ST
import Control.Monad.ST.Trans.Internal (STT (..), STTRet (..))
import Data.Functor
import Polysemy
import Polysemy.Internal
import Polysemy.Internal.Union
import Unsafe.Coerce (unsafeCoerce)
import Data.Functor.Compose
import Data.STRef (STRef)

data STE s :: Effect where
  NewSTRef   :: a -> STE s m (STRef s a)
  ReadSTRef  :: STRef s a -> STE s m a
  WriteSTRef :: STRef s a -> a -> STE s m ()

makeSem ''STE

runSTE :: forall r a . (forall s . Sem (STE s ': r) a) -> Sem r a
runSTE sem = ST.runSTT $ STT $ go sem where
  go :: forall r a s . Sem (STE s ': r) a -> State# s -> Sem r (STTRet s a)
  go (Sem sa) s = Sem \k -> let
    STT f = sa \u -> case decomp u of
      Left rest -> STT \s -> k $ weave
        (STTRet s ())
        (\(STTRet s sa) -> go sa s)
        (Just . \(STTRet _ a) -> a)
        rest
      Right (Weaving e fs d r _) -> case e of
        NewSTRef a -> r . (fs $>) <$> ST.newSTRef a
        ReadSTRef ref -> r . (fs $>) <$> ST.readSTRef ref
        WriteSTRef ref a -> r . (fs $>) <$> ST.writeSTRef ref a
    in f s

-- Does not typecheck
-- whoops :: forall s. STRef s Integer
-- whoops = run $ runSTE ref

ref :: forall s r. Member (STE s) r => Sem r (STRef s Integer)
ref = newSTRef 42

main :: IO ()
main = print $ run $ runSTE do
  r <- ref
  a <- readSTRef r
  writeSTRef r 43
  b <- readSTRef r
  pure (a, b)

[tek]

🧐

[tek]

@TheMatten can you do that with STM? 😳

[tek]

eh no, there's no safe analogue of ioToST for STM

[tek]

oh and this implementation doesn't even run in IO. nvm

[TheMatten]

@tek ST is just IO without interaction with outside world, so it should be fine as long as you don't introduce nondeterministic effects into the stack (no guarantees though 😅 ).
But I'm not too familiar with STM - it seems like it may be possible with atomically treated as an interpreter, joining resulting STM (Sem r a) into embedded IO?

[MaciekFlis]

@TheMatten thanks for this, I admit it took me few hours staring into this until I understood what's happening ;)

Tried to do this for my case, sadly I think I'm still out of luck, as my concrete effects have also MonadIO constraint, which propagate from Right branch, but Sem does not have it.
I'm not sure what's the workflow here, but this can be closed as far as I'm concerned.