Interpreters forcing empty effect lists

[Burtannia]

I've been experimenting with heftia a bit and noticed that the types of various interpreters force certain constraints on interpretation order. For example, the following evalState enforces that there are no existing higher order effects in the stack:

evalState :: forall s (ef :: [Type -> Type]) a. s -> Eff ('[] :: [EffectH]) (State s ': ef) a -> Eff ('[] :: [EffectH]) ef a

runCatch and runThrow have similar constraints.

On the other hand, runReader has a much more permissive type:

runReader :: forall r (eh :: [(Type -> Type) -> Type -> Type]) (ef :: [Type -> Type]). r -> Eff (Local r ': eh) (Ask r ': ef) ~> Eff eh ef

What confuses me more is that runStateIORef also has the permissive constraints:

runStateIORef :: forall s (ef :: [EffectF]) (eh :: [EffectH]) a. IO <| ef => s -> Eff eh (State s ': ef) a -> Eff eh ef (s, a)

What's the reason for these constraints? I'd assumed it was to prevent the footgun of interpreting effects in the wrong order and accidentally letting exceptions through. But then I'm confused as to why runStateIORef has the more permissive constraint? Or is it due to using an IORef, we get atomic state updates so can be more permissive than pure state?

If this is the case then I think that's a feature that needs to be stated more clearly, because, despite being a little confusing to new-comers, it's fantastic!

[zamphion]

https://github.com/sayo-hs/heftia/blob/master/heftia-effects/src/Control/Monad/Hefty/State.hs
some of the comments by author in the file ^ might explain it, ... I don't understand it completely, but if you
follow some of the comments and references made, it might get you to the answer. You might also want to
check out the freer-simple docs, as it might be telling what the diffs are.

[ymdfield]

This is a very core question regarding implementing algebraic effects in Haskell.

The runState/runStateNaive functions are purer and more "algebraic effects"-like, making their behavior easier to explain. If you’re not overly concerned with performance and the restrictions imposed by interpretation order aren't an issue, you should primarily use these. Otherwise, if you need performance tuning or wish to interpret higher-order effects after runState, consider using runStateIORef. This reasoning also applies to effects other than State (e.g. runThrow vs. runThrowIO).

Implementing algebraic effects purely makes the behavior straightforward, but as a trade-off, it imposes an interpretation order constraint—from higher-order to first-order effects. I don't fully understand why this ultimately is the case, but one thing is clear: it allows us to completely port the semantics from algebraic effects papers into Haskell. I currently see this as a kind of type safety in interpreting higher-order effects. Perhaps you might have already seen my article (see the "Essential Structure" section):

https://sayo-hs.github.io/jekyll/update/2024/09/04/how-the-heftia-extensible-effects-library-works.html

The restriction that higher-order effects must be fully interpreted before handling delimited continuations can be seen as a “type-level guardrail” that prevents unsafe behavior where things jump out of scope unexpectedly. If the types are structured this way, the type system ensures that before interpreting delimited continuations, all higher-order effects must be interpreted first. This order is guaranteed by the type system, allowing us to say goodbye to unpredictable, strange behavior.

I don't think atomic state updates are really related here. At the moment, I consider runStateIORef to be more of an impure hack. Anyway, it's a new approach, so there's still a lot to explore.

Detailed explanation:
runStateIORef uses an IORef internally―as is common in other effect libraries—so its behavior can be influenced by other IO-monad operations (throwIO, catchIO, forkIO, etc.). This behavior is often referred to in the documentation as "IO-fused semantics." With IO-fused semantics, programs involving IO exceptions and multithreading can become harder to explain, predict, and debug. However, since its behavior is identical to conventional imperative programming (as in Haskell's IO monad or C), it might feel more natural to those accustomed to that style.

In contrast, runState and runStateNaive implement state using the delimited continuation of algebraic effects. They are purer and adhere exactly to the semantics described in the documentation and related academic papers on algebraic effects. This is what researchers will consider the standard interpretation of state effects—essentially the "orthodox runState."

Ideally, this should be illustrated with concrete examples, but I apologize for not having a detailed investigation of the behavior yet. I hope to document it with examples in the future.

A minor note:
Performance optimizations (Control.Monad.Hefty.Interpret.State) complicate the discussion slightly. For now, I'm focusing solely on the behavior, meaning the discussion here pertains to runStateNaive. Although runState and runStateNaive differ in speed, their interfaces and semantics are completely equivalent.

[ymdfield]

By the way, having ef and eh separated is inconvenient, so in the next update (v0.6), they will be unified to something like Eff (es :: [Effect]) a instead of Eff eh ef a. The interpretation order constraint and distinction between first-order and higher-order effects remains, so the essential mechanism doesn't change. However, since the functions currently split between first-order and higher-order (interpret/interpretH) will be unified, the interface will become much simpler.

[ymdfield]

I've released version 0.6, and the interface is now unified.
https://hackage-content.haskell.org/package/heftia-0.6.0.0/docs/Control-Monad-Hefty.html

[ymdfield]

I am currently working on relaxing these constraints: #26 #27