unlift.md

Generalizing the unwrap/rewrap operation yields the following function:

withLogicToEff :: (forall e. (Logic es a -> Eff (e :& es) ()) -> Eff (e :& es) ()) -> Logic es a
withLogicToEff f = MkLogic \y -> f \m -> enumerate m y

It has a signature similar to MonadUnliftIO's withRunInIO:

withRunInIO :: MonadUnliftIO m => ((forall x. m x -> IO x) -> IO a) -> m a

In MonadUnliftIO, the base monad is IO and the upper monad is m. The function

run :: forall x. m x -> IO x

that transforms the upper monad into the base monad is passed as a callback, and we often call this operation unlift.

Similarly, in withLogicToEff, the base monad is Eff (e :& es) and the upper monad is Logic es.

When an unlift operation is possible, we can use existing interfaces designed to take the base monad as an argument with the upper monad. I will call this reuse.

For example, for the local function we can write:

local' :: (e :> es) => Reader r e -> (r -> r) -> Logic es a -> Logic es a
local' r f m = withLogicToEff \run -> local r f (run m)

However, the difference between withLogicToEff and withRunInIO is that the former cannot transform arbitrary forall x but fixes the return type of Eff to (). This isn't an issue in the local example, but we cannot properly reuse it for functions whose return type differs from their argument.

For example, the following functions (their counterparts in bluefin) apply:

• tryError: https://hackage.haskell.org/package/mtl-2.3.1/docs/Control-Monad-Except.html#v:tryError
• listen: https://hackage.haskell.org/package/mtl-2.3.1/docs/Control-Monad-Writer-Lazy.html#v:listen
• pass: https://hackage.haskell.org/package/mtl-2.3.1/docs/Control-Monad-Writer-Lazy.html#v:pass

Below is an example attempt to reuse Writer's listen (not implemented yet in bluefin but analogous):

listen :: (e :> es) => Writer w e -> Eff es a -> Eff es (a, w)

listen' :: (e :> es) => Writer w e -> Logic es a -> Logic es (a, w)
listen' writer m = withLogicToEff \run -> do
    ((), w) <- listen writer (run m) -- Couldn't match type ‘a’ with ‘(a, w)’
    pure ()

We might invent workarounds case by case, but covering all cases comprehensively seems difficult. In this sense, for the Logic monad, partial unlifting is indeed possible, but since full unlifting cannot be achieved, one could say that direct reuse is not possible.

Moreover, for effect-handling functions like runState or try, the type-level list of effects changes, meaning the e :& es part of the base monad Eff (e :& es) is not fixed, so reuse via unlift is impossible. Therefore, we need to consider other approaches, but as I will mention below, I could not find a method.

These challenges arise when designing by stacking a new monad on top of the existing Eff monad. On the other hand, libraries like fused-effects, freer-simple, or heftia that integrate non-deterministic computation (Logic) as an effect with the existing Eff avoid these issues and allow seamless reuse of existing interfaces without unlift.

Although there are such challenges, the ability to perform even partial unlifting is a capability not found in existing the list-t package or LogicT, so I still find it an interesting idea.

---

Finally,

https://x.com/tomjaguarpaw/status/1927356780582973562

If you have Logic defined in terms of effectful/Bluefin then you can handle the effects in any order.

Regarding this, I am not yet familiar with bluefin's type level list mechanism, so I do not know how. Sharing code that performs runState or try inside runLogic, like in the following code, would make it clear that it is possible, so I would appreciate that.

-- I want to write an effectful program like this, but I get type errors

testProgram :: (e :> es) => State String e -> Logic es Int
testProgram st = do
    () <- pure () <|> pure ()
    s <- get st
    put st "modified"
    pure $ length s

main :: IO ()
main =
    runEff \io -> ignoreStream \y -> runLogic y do
        (n, s) :: (Int, String) <-
            undefined -- I don’t know how to write this part
                $ runState "unmodified" testProgram
        liftEff $ effIO io $ print (n, s)

-- Expected output:
-- (10, "modified")
-- (10, "modified")

heftia ver: https://gist.github.com/ymdryo/ffb7038dfd6d755fa6dc2eebcc30edbb

Unfortunately what I wrote does not work. It breaks on even a slightly more complicated program. The output should be all 2, like the list example.

testProgram ::
  (e1 :> es) =>
  State Int e1 ->
  Logic es ()
testProgram st = do
  () <- pure () <|> pure ()
  liftEff (modify st (+ 1))
  () <- pure () <|> pure ()
  liftEff (modify st (+ 1))

-- ghci> main
-- ghci> main
-- 2
-- 1
-- 2
-- 1
main :: IO ()
main =
  runEff \io -> ignoreStream \y -> runLogic y do
    (_, s) <- runStateLogic 0 testProgram
    liftEff $ effIO io $ print s

import Control.Applicative ((<|>))
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.State (StateT, modify, runStateT)

testProgram :: StateT Int [] ()
testProgram = do
  () <- lift (pure () <|> pure ())
  modify (+ 1)
  () <- lift (pure () <|> pure ())
  modify (+ 1)

-- ghci> example
-- [2,2,2,2]
example :: [Int]
example = do
  (_, s) <- flip runStateT 0 $ do
    testProgram
  pure s