Can we write a mask effect?

[ocharles]

You thought I was done with just an Async effect?

I would like to know if it's possible to write

data Mask m a where
  Mask :: ( ( forall a. m a -> m a ) -> m b ) -> Mask m b

In my little toy work, I don't think what is essentially weave is sufficient to express such an effect. Ignore all functor stuff (or setting f = Identity), weave gives us:

(forall x. m x -> n x) -> e m a -> e n a

But given an m x -> n x, I don't believe you can write Mask m x -> Mask n x. Due to the nested functions, you will end up needing n x -> m x.

At this level of quantification, my brain begins to explode 😖 🤔

[isovector]

Why are you like this?

[isovector]

After staring at it for 15 minutes, I'm going to agree that I don't think this is doable. m is in invariant position wrt Mask, meaning we'd need an isomorphism: forall m. Monad m => Iso m (Sem r), which clearly we don't have.

But the deeper question here is "what the hell kind of thing are you actually trying to model?"

[ocharles]

But the deeper question here is "what the hell kind of thing are you actually trying to model?"

Nothing, I'm just trying to see what can and cannot be expressed within polysemy. We can express this in mtl - https://hackage.haskell.org/package/exceptions-0.10.2/docs/Control-Monad-Catch.html#v:mask for example. So it's worth understanding what we can and cannot think about in polysemy.

It is possible that this can be thought about in polysemy, but not in this current formulation. Edit: by "this formulation" I mean the current type of mask. Maybe we can have mask/restore in current polysemy - I don't know!

[isovector]

Okay, weird. I'm genuinely surprised by how many instances of MonadMask there are --- all of these seem like they should be subject to the same limitation wrt invariance. Maybe I'll look at it really hard for another 15 minutes.

[isovector]

I got it down to this:

    • Found hole: _ :: IO (f a2) -> m1 a2
      Where: ‘a2’ is a rigid type variable bound by
               a type expected by the context:
                 forall a2. m1 a2 -> m1 a2
               at /home/sandy/Vikrem.hs:(27,23)-(29,30)
             ‘f’, ‘m1’ are rigid type variables bound by
               a pattern with constructor:
                 Yo
      Constraints include
        Functor f (from /home/sandy/Vikrem.hs:26:14-37)
        Monad m (from /home/sandy/Vikrem.hs:(24,11)-(29,35))
        LastMember (Lift IO) r (from /home/sandy/Vikrem.hs:(19,1)-(22,14))

We know by construction that m1 is of the form Sem r0, and furthermore that LastMember (Lift IO) r0. But this isn't reified anywhere. If it were, the hole is just sendM . fmap inspect.

[isovector]

runMask
    :: LastMember (Lift IO) r
    => Sem (Mask ': r) a
    -> Sem r a
runMask (Sem m) = withLowerToIO $ \lower finish ->
  lower $ Sem $ \k -> m $ \u ->
    case decomp u of
      Right (Yo (Mask masked) s d y v) -> fmap y $ usingSem k $ do
        runMask $ d $ masked (\m1a2 ->
          _ $ lower $ runMask $ d $ m1a2 <$ s
                             ) <$ s

[isovector]

But in the meantime just use Bracket and scope your masked blocks like that -_-

[isovector]

I'm going to close this, and we can reinvestigate if someone comes up for a genuine use case. MonadMask exists solely to provide bracket semantics, which we already have via the Resource effect. Feel free to reopen if you think this is a tyrannical move.

[ocharles]

You could also imagine that mask is actually a handler for programs with an Unmask effect:

data Unmask m a where
  Unmask :: m a -> Unmask m a

mask :: Sem (Unmask ': es) a -> Sem es a
mask = ...

But I'm not sure if that's possible to write. Maybe it is though!

[KingoftheHomeless]

Just a note: a Mask effect that simply represents mask is indeed not implementable straight-up; however, it's possible to implement Mask through representing the primitives that are used to implement mask in the first place:

data Mask m a where
  Unblock              :: m a -> Mask m a
  Block                :: m a -> Mask m a
  BlockUninterruptible :: m a -> Mask m a
  GetMaskingState      ::        Mask m MaskingState

mask :: Member Mask r => ((forall x. Sem r x -> Sem r x) -> Sem r a) -> Sem r a
mask main = send GetMaskingState >>= \case
  Unmasked -> send $ Block $ main (\x -> send (Unblock x))
  MaskedInterruptible -> main (\x -> send (Block x))
  MaskedUninterruptible -> main (\x -> send (BlockUninterruptible x))

Interpreting mask through Final IO requires reimplementing the block :: IO a -> IO a and blockInterruptible :: IO a -> IO a primitives, as GHC.IO doesn't export them.

maskToIOFinal :: Member (Final IO) r => Sem (Mask ': r) a -> Sem r a
maskToIOFinal = interpretFinal @IO $ \case
  Unblock m -> do
    m' <- runS m
    pure $ GHC.IO.unsafeUnmask m'
  Block m -> do
    m' <- runS m
    pure $ block m'
  BlockUninterruptible m -> do
    m' <- runS m
    pure $ blockUninterruptible m'
  GetMaskingState -> liftS GHC.IO.getMaskingState

An easier approach if we don't want to bother with an intermediary effect is to use Final IO directly:

mask :: forall r a. Member (Final IO) r => ((forall x. Sem r x -> Sem r x) -> Sem r a) -> Sem r a
mask main = withWeavingToFinal $ \s wv _ -> Control.Exception.mask $ \restore ->
  let
    restore' :: forall x. Sem r x -> Sem r x
    restore' m = withStrategicToFinal $ do
      m' <- runS m
      pure $ restore m'
  in
    wv (main restore' <$ s)

So a Mask effect, or a mask action through Final IO, are both possible if ever needed.

[KingoftheHomeless]

There's a general pattern I've discovered for creating effects for actions that have contravariant occurrences of m like this: namely, using an intermediary type variable.
Applying this to Mask, we can get the following effect, which we may interpret using mask directly:

import qualified Control.Exception as X

data Mask s m a where
  Mask' :: (s -> m a) -> Mask s m a
  Restore' :: s -> m a -> Mask s m a

mask
  :: Member (Mask s) r
  => ((forall x. Sem r x -> Sem r x) -> Sem r a)
  -> Sem r a
mask main = send $ Mask' $ \s -> main (\m -> send (Restore' s m))

newtype Restoration = Restoration (forall x. IO x -> IO x)

runMask
  :: Member (Final IO) r
  => Sem (Mask Restoration ': r) a
  -> Sem r a
runMask = interpretFinal $ \case
  Restore' (Restoration restore) m ->  do
    m' <- runS m
    pure $ restore m'
  Mask' main -> do
    main' <- bindS main
    s <- getInitialStateS
    pure $ X.mask $ \restore -> main' (Restoration restore <$ s)

The downside is, of course, the need for an intermediary variable.

To give another example of how this pattern may be applied, it can be used to formulate Cont in a more intuitive way than using the more clumsy Jump/Subst formulation, which was tailor-made to be implementable using standard algebraic effects (although both formulations require a type variable).

import Control.Monad.Cont (MonadCont)
import qualified Control.Monad.Cont as C

data Cont s m a where
  Abort :: s -> Cont s m a
  CallCC' :: ((a -> s) -> m a) -> Cont s m a

callCC
  :: Member (Cont s) r
  => ((forall b. a -> Sem r b) -> Sem r a)
  -> Sem r a
callCC cc = send $ CallCC' $ \c -> cc (\a -> send (Abort (c a)))

contToFinal :: (Member (Final m) r, MonadCont m)
            => Sem (Cont (m Void) ': r) a
            -> Sem r a
contToFinal = interpretFinal $ \case
  Abort s -> pure $ vacuous s
  CallCC' main -> do
    main' <- bindS main
    s <- getInitialStateS
    pure $ C.callCC $ \exit -> main' ((exit . (<$ s)) <$ s)

You can also use this pattern to create an effect for MonadLogic:

data Logic s m a where
  Recall :: s a -> Logic s m a
  Split' :: m a -> Logic s m (Maybe (a, s a)) 

split
  :: Member (Logic s) r
  => Sem r a
  -> Sem r (Maybe (a, Sem r a))
split m = (fmap . fmap . fmap) (send . Recall) $ send (Split' m)

(Interpreting this is a bit dicey though; it forces you to use the inspector).

[ocharles]

https://github.com/fused-effects/fused-effects/blob/71d8468fa8f63d93c36a45452c178d395fc4d5c3/src/Control/Effect/Exception.hs#L162 suggests this might actually be possible. See fused-effects/fused-effects#306 for a very cool more powerful Lift effect. Can polysemy do this too?

[ocharles]

Actually, I'm not sure the fused-effects stuff let's us define a Mask effect, but rather just gives us a way to lift IO's mask. But maybe there's something there.

[KingoftheHomeless]

fused-effects's new Lift is our Final.

That means it's possible for them to write Mask like I showed above.

[ocharles]

Thanks for helping me associate them!