Rearranging effect order

[chris-martin]

Is it possible to define the following function?

swap :: Eff (e1 ': e2 ': es) a -> Eff (e2 ': e1 ': es) a

I had hoped I might be able to write:

swap = inject

But the error I get is:

No instance for (Subset es (e2 : e1 : es)) arising from a use of ‘inject’

... which is disappointing, because clearly any es must always be a subset of ... : es.

[arybczak]

Currently inject only works if you deal with monomorphic stacks (as then GHC just solves the constraint) or if you pass the Subset evidence around.

This isn't particularly satisfying and I'm pretty sure through a clever trick Subset can be modified to auto resolve with stacks that share an opaque tail, I just didn't look at this in depth yet.

[arybczak]

Yes, but it's not very pretty 🙂

import Data.Primitive.PrimArray
import Effectful.Internal.Env
import Effectful.Internal.Monad

swap :: Eff (e1 : e2 : es) a -> Eff (e2 : e1 : es) a
swap m = unsafeEff $ \es -> unEff m =<< swapEnv es
  where
    swapEnv :: Env (e1 : e2 : es) -> IO (Env (e2 : e1 : es))
    swapEnv (Env offset refs0 storage) = do
      let size = sizeofPrimArray refs0 - offset
      mrefs <- newPrimArray size
      copyPrimArray mrefs 4 refs0 (offset + 4) (size - 4)
      writePrimArray mrefs 0 $ indexPrimArray refs0 (offset + 2)
      writePrimArray mrefs 1 $ indexPrimArray refs0 (offset + 3)
      writePrimArray mrefs 2 $ indexPrimArray refs0 (offset + 0)
      writePrimArray mrefs 3 $ indexPrimArray refs0 (offset + 1)
      refs <- unsafeFreezePrimArray mrefs
      pure $ Env 0 refs storage

[chris-martin]

Fascinating. Thank you!

[arybczak]

@chris-martin FWIW, if you're using this, the original version was wrong (it didn't take offset into account when swapping). I updated the code above.

The original worked fine as long as you didn't use raise.

[ocharles]

@arybczak Am I right in thinking that @chris-martin could now just use swap = inject as originally intended?

[arybczak]

Yes, with a caveat - you can swap any two concrete effects, but unfortunately you can't use it to implement a generic swap.

>>> swap :: Eff (e1 : e2 : es) a -> Eff (e2 : e1 : es) a; swap = inject

<interactive>:1:62: error:
    • Overlapping instances for e1 :> (e2 : e1 : es)
        arising from a use of ‘inject’
      Matching instance:
        instance (e :> es) => e :> (x : es)
          -- Defined at src/Effectful/Internal/Effect.hs:55:10
      Potentially matching instance:
        instance [overlapping] e :> (e : es)
          -- Defined at src/Effectful/Internal/Effect.hs:52:30
      (The choice depends on the instantiation of ‘e2, e1, es’
       To pick the first instance above, use IncoherentInstances
       when compiling the other instance declarations)
    • In the expression: inject
      In an equation for ‘swap’: swap = inject

Because GHC doesn't know whether e1 and e2 are the same or not 😞