interpreting into a different type - Polysemy

hi guys! im learn polysemy and am looking to get some practice. to do that i have been trying to reimplement some of the stuff in the paper "Effect handlers in scope"
however, when trying to replicate one of the first examples (the nondet computation one), i ran into some issues

essentially im looking to write an interpreter for this effect:

data Backtrack m a where
    BtNode :: a -> Backtrack m a
    BtFail :: Backtrack m a
    BtChoice :: m a -> m a -> Backtrack m a

makeSem ''Backtrack

runBacktrack :: Sem (Backtrack ': r) a -> Sem r [a]

the problem i have is implementing runBacktrack, which interprets into a different return type ([a] rather than a). i run into errors when trying to use the standard interpret/interpretH functions - with interpret I've the problem that its first parameter interprets into the same type a: e Sem (e ': r) a -> Sem r a

and with interpretH I think I'm still a bit confused about its usage - I had issues coming up with return values satisfying forall f

looking at the existing examples on State (another example where handled type differs from original), it seems like there's some custom interpret-like function written for that special case

if I want to do something like Backtrack, is that what I must do as well? or is there a way to make it work with interpretH?

(State example I'm referring to: https://github.com/polysemy-research/polysemy/blob/master/src/Polysemy/State.hs ,
and Effect handlers in scope paper: https://www.cs.ox.ac.uk/people/nicolas.wu/papers/Scope.pdf - I'm trying to implement the solutions handler at the end of chapter 3)

yes, if you want to change the return type you'll have to crack open the Sem manually. maybe start by inlining interpretH or runError and playing type tetris.

In the next release, this will likely become easier, but it's gonna take some more time

thanks torsten! that helps a lot - i'll stop fiddling with interpretH, trying to make it work for now :)

hello! so i've been playing type puzzles over the last couple days and i ended up with something like below for the "interpretList" function

interpretAsListT
    :: (forall x m. e m x -> ListT (Sem r) x)
    -> [Sem (e ': r) a] -- s (m a)
    -> Sem r [a]        -- n (s a)
interpretAsListT nt sems = Sem $ \k -> do
        xss <- mapM (interpretIntoList_ k nt) sems
        return $ concat xss

interpretIntoList_
    :: (Monad m) =>
    (forall x. Union r (Sem r) x -> m x)
    -> (forall x m. e m x -> ListT (Sem r) x)
    -> Sem (e ': r) a
    -> m [a]
interpretIntoList_ k nt (Sem m) = m $ \u ->
    case decomp u of
        Left  y -> k $ weave [] (interpretAsListT nt) maybeHead $ y
        Right (Weaving e s d y v) -> runListT (nt e) & usingSem k & fmap y
    where
        maybeHead :: [a] -> Maybe a
        maybeHead (x:xs) = Just x
        maybeHead []     = Nothing

however, it doesn't quite compile and the error message i get really got me stuck - despite the types seem to fit together on pen&paper, far as i can tell. for the Left case in particular, the complaint is that weave returns an Union r (Sem r) [a], which k doesn't accept for some reason despite it being a natural transformation forall x. Union r (Sem r) x -> m x. Wondering if anyone could offer some hints / pointers?

you have to weave the transformer through the application of the handler:

interpretIntoList_
    :: (Monad m) =>
    (forall x. Union r (Sem r) x -> m x)
    -> (forall x m. e m x -> ListT (Sem r) x)
    -> Sem (e ': r) a
    -> m [a]
interpretIntoList_ k nt (Sem m) = runListT $ m $ \u ->
    case decomp u of
        Left  y -> ListT $ k $ weave [] (interpretAsListT nt) maybeHead $ y
        Right (Weaving e s d y v) -> nt e & mapListT (usingSem k) & fmap (y . (<$ s))
    where
        maybeHead :: [a] -> Maybe a
        maybeHead (x:xs) = Just x
        maybeHead []     = Nothing

so that ListT is returned on the "inside" of the m and unwrapped outside, since m returns a concrete a, while your [a] is what the transformer's state "hides".

Note that nondeterminism is really hairy with polysemy, you might want to look at previous discussions about the topic.

thank you so much for this torsten! It's getting late tonight but I will study this more tomorrow to digest the solution, and thanks for that thread also! :)

sorry to come back after so long - the function compiled and I moved on for a while to other tasks, thinking it's all working fine..
however earlier today i was just looking back into the code and tried to use it in handler implementations as follows:

runBacktrack :: [Sem (Backtrack ': r) a] -> Sem r [a]
runBacktrack = interpretAsListT $ \case
    BtNode x -> ListT $ return [x]
    BtFail -> ListT $ return []
    BtChoice bta btb -> ListT $ do
        as <- runBacktrack [bta]
        bs <- runBacktrack [btb]
        return $ as ++ bs

interpretAsListT
    :: (forall rInitial x. e (Sem rInitial) x -> ListT (Sem r) x)
    -> [Sem (e ': r) a] -- s (m a)
    -> Sem r [a]        -- n (s a)
interpretAsListT nt sems = Sem $ \k -> do
        xss <- mapM (interpretIntoList_ k nt) sems
        return $ concat xss

interpretIntoList_
    :: (Monad m) =>
    (forall x. Union r (Sem r) x -> m x)
    -> (forall rInitial x. e (Sem rInitial) x -> ListT (Sem r) x)
    -> Sem (e ': r) a
    -> m [a]
interpretIntoList_ k nt (Sem m) = runListT $ m $ \u ->
    case decomp u of
        Left  y -> ListT $ y & weave [] (interpretAsListT nt) maybeHead & k
        Right (Weaving e s d y v) -> nt e & mapListT (usingSem k) & fmap (y . (<$ s))
    where
        maybeHead :: [a] -> Maybe a
        maybeHead (x:xs) = Just x
        maybeHead []     = Nothing

which complains about

Couldn't match type ‘rInitial’ with ‘Backtrack : r’
  Expected: Sem (Backtrack : r) x
    Actual: Sem rInitial x"

in the line as <- runBacktrack [bta]

im really sorry for my ignorance, but I am having trouble understanding this complain: isn't rInitial ~ Backtrack ': r exactly what we wanted?

Jacob Yu said:

im really sorry for my ignorance, but I am having trouble understanding this complain: isn't rInitial ~ Backtrack ': r exactly what we wanted?

right, this is not precisely true: the Weaving carries the tools to transform rInitial to Backtrack : r. Any higher-order effect interpreter has to apply the previous handlers to all chunks with d, so you'll have to pass that to your Backtrack handler:

runBacktrack :: [Sem (Backtrack ': r) a] -> Sem r [a]
runBacktrack = interpretAsListT \ d -> \case
    BtNode x -> ListT $ return [x]
    BtFail -> ListT $ return []
    BtChoice bta btb -> ListT $ do
        as <- runBacktrack [d bta]
        bs <- runBacktrack [d btb]
        return $ catMaybes (as ++ bs)

interpretAsListT
    :: (forall rInitial x. (∀ y . Sem rInitial y -> Sem (e : r) (Maybe y)) -> e (Sem rInitial) x -> ListT (Sem r) x)
    -> [Sem (e ': r) a] -- s (m a)
    -> Sem r [a]        -- n (s a)
interpretAsListT nt sems = Sem $ \k -> do
        xss <- mapM (interpretIntoList_ k nt) sems
        return $ concat xss

interpretIntoList_
    :: (Monad m) =>
    (forall x. Union r (Sem r) x -> m x)
    -> (forall rInitial x. (∀ y . Sem rInitial y -> Sem (e : r) (Maybe y)) -> e (Sem rInitial) x -> ListT (Sem r) x)
    -> Sem (e ': r) a
    -> m [a]
interpretIntoList_ k nt (Sem m) = runListT $ m $ \u ->
    case decomp u of
        Left  y -> ListT $ y & weave [] (interpretAsListT nt) maybeHead & k
        Right (Weaving e s d y v) -> (nt (fmap v . d . (<$ s))) e & mapListT (usingSem k) & fmap (y . (<$ s))
    where
        maybeHead :: [a] -> Maybe a
        maybeHead (x:xs) = Just x
        maybeHead []     = Nothing

This is not necessary for State, since that is not a higher order effect. A better example would be interpretViaLazyWriter.
The updated code is getting pretty messy with the interpreters being passed around – as you can see in the Writer example, it might be easier to pass the entire Weaving to nt instead of the e.
Note that this new function d produces a Maybe – this represents the case where a previous interpreter produced a failed state, for example when interpreting Error into ExceptT and getting a Left from throwing.