Encode effect in terms of another with freer extensible effects

I have been playing around with “freer monads” and extensible effects, implemented in the freer-effects package, and I’ve run into a problem that seems feasible but I’m having trouble solving.

I’ve written a type that represents simple interactions with a file system:

data FileSystem v where
  ReadFile :: FilePath -> FileSystem String
  WriteFile :: FilePath -> String -> FileSystem ()

Writing an interpreter for this in IO is easy, but boring. What I’m really interested in doing is writing a pure interpreter that uses State internally. I could effectively inline the implementation of runState into my interpreter for FileSystem, but that seems like it would sort of defeat the purpose. What I’d really like to be able to do is write a transformation between these two types, then reuse the State interpreter.

Writing such a transformation is straightforward:

fsAsState :: forall v r. FileSystem v -> Eff (State [(FilePath, String)] ': r) v
fsAsState (ReadFile a) = (lookup a <$> get) >>=
  maybe (fail "readFile: file does not exist") return
fsAsState (WriteFile a b) = modify $ \fs ->
  (a, b) : filter ((/= a) . fst) fs

Now I want a generic reencode function that can accept my fsAsState transformation and use it to interpret my FileSystem by reusing the State interpreter. With such a function, I would be able to write the following interpreter:

runInMemoryFS :: forall r w. [(FilePath, String)] -> Eff (FileSystem ': r) w -> Eff r (w, [(FilePath, String)])
runInMemoryFS fs m = runState (reencode fsAsState m) fs

The tricky thing is actually implementing reencode. I’ve gotten something that almost typechecks:

reencode :: forall r w f g. (forall v. f v -> Eff (g ': r) v) -> Eff (f ': r) w -> Eff (g ': r) w
reencode f m = loop m
  where
    loop :: Eff (f ': r) w -> Eff (g ': r) w
    loop (Val x) = return x
    loop (E u q) = case decomp u of
      Right x -> qComp q loop =<< f x
      Left u' -> E (weaken u') undefined

Unfortunately, I can’t figure out how to provide the second argument to E in the final case of loop. I don’t think I understand the implementation details of how the optimized FTCQueue type works in order to understand if there’s something I need to do here that is simple, or if what I’m doing is just impossible.

Is this possible? If the answer is no, and it turns out that what I’m doing is, in fact, impossible, I would be interested in an explanation to help me understand why.

Solution

DISCLAIMER: the below typechecks but I haven't tried running it.

You need to walk q (from the E u q pattern match) and shift all its steps from Eff (f ': r) to Eff (g ': r). We can write this traversal polymorphically:

shiftQ :: forall m n a b. (forall a. m a -> n a) -> FTCQueue m a b -> FTCQueue n a b
shiftQ shift q = case tviewl q of
    TOne act -> tsingleton (shift . act)
    act :| q -> go (tsingleton (shift . act)) q
  where
    go :: forall a b c. FTCQueue n a b -> FTCQueue m b c -> FTCQueue n a c
    go q' q = case tviewl q of
        TOne act -> q' |> (shift . act)
        act :| q -> go (q' |> (shift . act)) q

(it's a bit awkward because we can only snoc and only uncons FTCQueues).

and then we can use it in reencode by passing reencode f itself as the shifter:

reencode :: forall r w f g. (forall v. f v -> Eff (g ': r) v) -> Eff (f ': r) w -> Eff (g ': r) w
reencode f m = loop m
  where
    loop :: Eff (f ': r) w -> Eff (g ': r) w
    loop (Val x) = return x
    loop (E u q) = case decomp u of
      Right x -> qComp q loop =<< f x
      Left u' -> E (weaken u') (shiftQ (reencode f) q)