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

I see! The point is that runState should be able to run unmodified even within the scope of a runLogic/runNonDet, and it should run each branch of the non-det with a fresh state each time. No, Bluefin's Logic can't do that. Here I wrote a special runStateLogic to deal with that[1]; then the code for main is the same as your version in heftia.

So yes, I think this is right:

We might invent workarounds case by case, but covering all cases comprehensively seems difficult.

I don't rule out the possibility of a general solution to this issue, but I don't know what that would be. So, for an answer to the question "what is LogicT for?" here is a fragment of an answer:

We want to be able to write runState s (a1 <|> a2) and have this mean the same as runState s a1 <|> runState s a2, which is useful for modularity

I'd like to see a collection of real-world examples of writing code like this before I decide how Bluefin should deal with it.

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE BlockArguments #-}

import Bluefin.Compound (mapHandle, useImpl, useImplIn, useImplUnder)
import Bluefin.Eff (Eff, runEff, (:&), (:>))
import Bluefin.IO (effIO)
import Bluefin.Internal (b, has, weakenEff)
import Bluefin.State (State, evalState, get, put)
import Bluefin.Stream (Stream, forEach, ignoreStream, yield)
import Control.Applicative (Alternative, empty, (<|>))
import Control.Monad (ap)

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

-- ghci> main
-- (10,"modified")
-- (10,"modified")
main :: IO ()
main =
  runEff \io -> ignoreStream \y -> runLogic y do
    (n, s) <- runStateLogic "unmodified" testProgram
    liftEff $ effIO io $ print $ (n, s)

-- Need a special state handler for running stateful Logics
runStateLogic ::
  s ->
  (forall e. State s e -> Logic (e :& es) r) ->
  Logic es (r, s)
runStateLogic s k =
  MkLogic $ \y' -> do
    evalState s $ \st ->
      forEach
        (\y -> runLogic y (weakenLogic (useImplUnderLogic (k st))))
        ( \r -> do
            s' <- get st
            yield y' (r, s')
            put st s
        )

-- This is messy. Need to come up with a better story.
mapLogic :: (e :> es) => Logic e a -> Logic es a
mapLogic (MkLogic k) = MkLogic (\y -> useImplUnder (k y))

weakenLogic :: Logic e1 a -> Logic (e2 :& e1) a
weakenLogic = mapLogic

useImplUnderLogic ::
  (e :> es) =>
  Logic (e1 :& e) r ->
  Logic (e1 :& es) r
useImplUnderLogic (MkLogic k) =
  MkLogic (\y -> weakenEff (b (b has)) (k y))

-- Logic definition

newtype Logic es a = MkLogic {enumerate :: forall e. Stream a e -> Eff (e :& es) ()}

instance Functor (Logic es) where
  fmap f (MkLogic k) =
    MkLogic (\y -> forEach (useImplUnder . k) $ \a -> yield y (f a))

instance Applicative (Logic es) where
  pure a = MkLogic (\y -> yield y a)
  (<*>) = ap

instance Monad (Logic es) where
  return = pure
  MkLogic k >>= f = MkLogic $ \y -> do
    forEach (useImplUnder . k) $ \a -> do
      enumerate (f a) y

instance Alternative (Logic es) where
  empty = MkLogic (\_ -> pure ())
  MkLogic p1 <|> MkLogic p2 = MkLogic $ \y -> do
    p1 y
    p2 y

runLogic :: (e :> es) => Stream a e -> Logic es a -> Eff es ()
runLogic y l = useImplIn (enumerate l) (mapHandle y)

-- This was corrected
liftEff :: Eff es a -> Logic es a
liftEff m = MkLogic $ \y -> do
  a <- useImpl m
  yield y a

---

[1] N.B. That it doesn't require Bluefin internals to write

Thank you for the code! It's nice that it can be written without relying on internal functions.

I'd like to see a collection of real-world examples of writing code like this before I decide how Bluefin should deal with it.

I agree, having more real-world examples would be very helpful when it comes to designing it.
I suspect there are things like mathematical solvers and parsers (though I’m not sure I could write those very well…)

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