interpreting into a different type - Polysemy

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Jacob Yu

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

Jacob Yu

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]
Jacob Yu

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

Jacob Yu

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

Jacob Yu

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

Jacob Yu

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?

Jacob Yu

(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)

Torsten Schmits

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

Jacob Yu

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

Jacob Yu

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?

Torsten Schmits

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.

Jacob Yu

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! :)