[question]How to implement a standard effect handler?

[myuon]

I want to implement an effect handler, using operation pattern-matching with continuations. For example, here is a simple state example:

interface State s = Get : s | Put : s -> ()

state : Eff [State a] r -> a -> r
state = \case
  value r -> \_ -> r
  <Get -> k> -> \s -> state (k s) s
  <Put s' -> k> -> \_ -> state (k ()) s'

In this example, type of the two continuation k in case pattern should be a -> Eff [State a] r and () -> Eff [State a] r.

However, peelEff has type Rebinder xs r -> (a -> r) -> (forall x. t x -> (x -> r) -> r) -> Eff ((k >: t) ': xs) a -> r, this seems not fit in this example. The type of operation handling function should be forall x. t x -> (x -> Eff xs r) -> r.

So how to implement this effect handler in extensible?

[fumieval]

Is peelEff1 what you want?

data GetPut s a where
   Get :: GetPut s s
   Put :: s -> GetPut s ()

runGetPut :: Eff ((k >: GetPut s) ': r) a -> s -> Eff r (a, s)
runGetPut = peelEff1 (\a s -> return (a, s))
  $ \t k s -> case t of
    Get -> k s s
    Put s' -> k () s'

[myuon]

Oh, Great! I just didn't understand how peelEff works. Thanks :smiley: