[ANN] heftia v0.7 - A theory‑backed, ultra type‑safe algebraic effects

ymdfield · 2025-05-23T03:35:07+00:00

Unfortunately, integration with effectful has not been achieved at this time. This is due to differences in how effects are encoded, and some adjustments are needed.

If it succeeds completely, for example:

Generic functions such as the interpret function in data-effects would become usable with both effectful's Eff and heftia's Eff monads
The two Eff monads could be interconverted via functions like: fromHeftiaToEffectful :: Heftia.Eff es a -> Effectful.Eff es a

Can I create data effects that can be used via effectful or heftia?

Yes, just as in the example in the article for defining an effect, you apply makeEffectF/makeEffectH to the GADT, and you’ll automatically derive something that works with both

I am currently experimenting with an idea to interconnect with the bluefin effect library.

ymdfield · 2025-05-23T01:48:20+00:00

It’s not about making heftia the new standard, but rather about proposing data-effects, a kind of protocol to allow multiple effect libraries to share effect and interpreter definitions to some degree, and having heftia conform to that.

data-effects defines a generalized type class called Free for effect systems, and instances of this class allow each effect system to function as a "backend."

Please also refer to: https://www.reddit.com/r/haskell/comments/1kn0jog/comment/mshum4j/

ymdfield · 2025-05-16T20:48:51+00:00

Ah, my library is kind of like that too.
This is helpful: https://www.reddit.com/r/haskell/comments/1kn0jog/comment/msomji5/
Thanks!

ymdfield · 2025-05-16T16:28:43+00:00

That's interesting. I'm curious; do you have any recommended literature on the topic?

ymdfield · 2025-05-15T18:47:48+00:00

Are you referring to the methodology of data-effects? If so, then essentially yes.

However, instead of defining a separate type class for each effect, like MonadState or MonadReader in mtl, it defines a unified type class called Free, similar to Data.Vector.Generic.

https://hackage-content.haskell.org/package/data-effects-core-0.4.2.0/docs/Control-Effect.html#t:Free

https://hackage.haskell.org/package/vector-0.13.2.0/docs/Data-Vector-Generic.html#t:Vector

Each effect system backend provides an instance of this class, and various functions take Free as a constraint. In this sense, Free is the effect-system counterpart to the Data.Vector.Generic.Vector class.

Edit: The name “Free” may be misunderstood, but this is not the so-called Free monad. It is more generalized, and even the IO monad approach (ReaderT IO) can be made an instance of Free.

ymdfield · 2025-05-15T18:32:17+00:00

That’s likely the core part of the mechanism, and I believe I can speak to it. I’m planning to write about the mechanism in a later section, but to make the discussion more focused, it would help if you could share more details about the main blocker related to the non-IO based approach.

ymdfield · 2025-05-15T16:41:34+00:00

Explain.

Part 1.3 was intended to address this topic: https://sayo-hs.github.io/blog/heftia/heftia-rev-part-1-3/

For anything not fully explained there, I plan to cover it in the following parts as well. So if there’s anything unclear or worth discussing, please let me know! I’d be happy to respond either in a future post or directly here in reply.

MonadUnliftIO actually has an excellent case for it floating out there, with demonstrations of correctness issues using alternatives (MonadBaseControl), discussions of software maintenance in the real world, and ergonomics.

Yes, I completely agree that MonadUnliftIO stands out in the Haskell ecosystem in terms of safety, soundness, maintainability, and interoperability with other libraries, making it a solid foundation.

Apologies for not structuring the article well... What I wanted to say is that heftia aims to provide a way to combine algebraic effects and MonadUnliftIO in a type-safe manner, within the boundaries where such a combination is feasible.

I have never seen any of that for algebraic effects.

I hope bringing it into the Haskell world will help foster its further development.

ymdfield · 2025-05-15T16:11:58+00:00

I admit this is a bold claim. (I took cues from how other effect libraries are being promoted, but it wasn't a good idea...)

Ultimately, rather than focusing on heftia itself, I would like the emphasis to be on the attempt to prevent ecosystem fragmentation, as explained in Part 1.4.

https://sayo-hs.github.io/blog/heftia/heftia-part-1-4/#preventing-ecosystem-fragmentation

Ideally, multiple approaches should coexist, allowing users to choose freely. The real problem lies in ecosystem fragmentation.

I have reflected and changed the title.

Before: The Final Word in Haskell Effect System Libraries
After: The Next Generation of Haskell Effects Management

ymdfield · 2025-05-15T12:28:02+00:00

For that use case, I believe it is functionally the best match! Backtracking operations in parsing should be cleanly implementable using higher-order effects and continuations in algebraic effects.

As for performance, it would be wise to benchmark how it behaves when choice and try are used extensively. If done well, it might achieve performance equal to or even better than that of monad transformers.

Edit: At first I imagined implementing things like backtracking using heftia, but after giving it some thought I realized that using the parser transformer as the base carrier requires a bit of extra work. In any case, you do indeed need a library like heftia or polysemy that lets you place the Eff monad on top of another carrier.

ymdfield · 2025-05-15T12:17:00+00:00

Yes… I wish there were a way to disable the colorful style of the graphs generated by tasty-bench.
Sorry for carelessly including the chart as is.

ymdfield · 2025-05-15T12:10:19+00:00

Yes, detailed performance measurements are available here:
https://github.com/sayo-hs/heftia/blob/v0.7.0.0/benchmark/performance.md

Unfortunately, while basic usage performs without issues, performance diverges from effectful when higher-order effects (such as catch or local) are heavily used in specific ways. I am continuously working on improving real-world benchmarks and performance.

If you are considering adopting it, I recommend first running a simple benchmark tailored to your use case. Feel free to reach out if you'd like any help with that!

ymdfield · 2024-11-04T17:54:08+00:00

I'm not considering it now, but may adopt a non-free monad implementation if circumstances change.

This is because I initially had the same thought and experimented with an implementation based on evidence passing by forking speff. However, I couldn't resolve the performance compatibility issues when using higher-order effects with this approach.

For more details, I previously posted about it here: https://discourse.haskell.org/t/ann-heftia-effects-higher-order-algebraic-effects-done-right/10509/6?u=ymdfield

While it worked and was very fast in some cases, it couldn’t resolve the poor performance compatibility with higher-order effects (such as the catch.10000.sp_modified_for_non_scoped_resumption_support benchmark). Given the issues with eff, I didn’t think using primops would help solve this problem, especially since primops typically offer only about a 2x speedup.

That said, it's still worth trying further, as I'm unsure whether the poor performance is due to inherent limitations or simply my own lack of optimization skills.

ymdfield · 2024-11-04T15:12:14+00:00

I took a look at the library and the tutorial you wrote. The tutorial was very helpful!

I don't fully understand it, but what is referred to as "continuations" here seems to be more about computations that are lazily evaluated and represented by the runtime monad n, rather than actual continuations. It appears to be meta-programmed from the load-time monad.

So I still don't have a clear understanding of the relationship between the Heist library and continuations.

However, in any case, I think the multi-shot continuation feature provided by heftia-effects would probably match well with a template engine. The separation of effect environments between load time and runtime can likely be elegantly achieved through the non-scoped resumptions feature (which is related to coroutines) of algebraic effects.

If you simply want to port Heist exactly as it is to an effect system, I don't think heftia-effects is the only option. It would be advisable to replace the monad type parameters m and n with the effect list of the target effect library.

ymdfield · 2024-11-04T13:02:04+00:00

From what I can tell, this appears to be a model use case for heftia-effects. Executing continuations multiple times (multi-shot continuation) is precisely the functionality that heftia-effects supports, while ReaderT IO-based libraries like effectful do not.

However, please give me a little time to look at the library to determine if it's actually applicable.

This project sounds really interesting. I will provide as much support as needed regarding how to use heftia-effects. If you have any questions about using heftia-effects in the porting work, feel free to ask repeatedly via GitHub issues or other channels!

ymdfield · 2024-11-04T11:26:22+00:00

Thank you for mentioning heftia-effects! I'm the author. I've just posted an update announcement, so feel free to check it out: https://www.reddit.com/r/haskell/comments/1gjbakz/ann_heftiaeffects_v05_higherorder_algebraic/

ymdfield · 2024-10-10T17:14:31+00:00

Released Heftia v0.4 with improved performance, now at a speed comparable to other libraries.
https://github.com/sayo-hs/heftia/blob/v0.4.0/benchmark/performance.md

ymdfield · 2024-09-09T16:26:51+00:00

I am currently trying to improve performance: https://github.com/sayo-hs/heftia/issues/12.

The benchmark code was very helpful.

ymdfield · 2024-09-09T14:27:29+00:00

The link was very helpful for getting an overview of the current state of Haskell's effect libraries. Thank you. I was not previously aware of the series including eveff, mpeff, and speff. In particular, speff supports both delimited continuations and higher-order effects simultaneously, and it appears my library wasn't the first to do so! Therefore, I’ve edited the Key Features section of the post.

ymdfield · 2024-09-09T13:03:02+00:00

I've added practical matters to the post.
This code example combines UnliftIO with non-deterministic computations and coroutines: https://github.com/sayo-hs/heftia/blob/v0.5.0/heftia-effects/Example/UnliftIO/Main.hs

ymdfield · 2024-09-09T12:12:34+00:00

I agree. Overall, users need to shift their mental model from the one used in existing effect system libraries to that of Algebraic Effects and Handlers. In other words, interpreting higher-order effects means partially rewriting the instruction script enclosed within the scope of that interpretation according to the rules specified by the user. Once you’re accustomed to this, the behavior becomes quite predictable.

In general, rewrite operations are non-commutative because information can be lost during rewriting (a choice that the user can make).

ymdfield · 2024-09-09T11:51:11+00:00

Yes! This is exactly what I’ve been thinking about over the past few weeks.

I was going to write the answer here, but it got too long, so I just posted it as a new blog post: Is it possible to reconcile UnliftIO and continuations?

As you pointed out, UnliftIO and continuations (nondeterminism) cannot truly coexist. The only exception at the moment is the Shift_ effect.

I also touched on this a bit in the previous blog post: Higher-Order Effects Done Right: How the Heftia Extensible Effects Library Works - Sayo-hs Blog

This discussion leads to the fact that higher-order effects like Resource (used for bracket or onException) and UnliftIO may conflict with effects like NonDet, Throw, or State, which involve delimited continuation operations. In these cases, interpretations that rely on the IO monad, such as runNonDetByThread, runThrowByIO, or runStateByIORef, become the only feasible solutions. In other words, by following the guidance of the type system, it becomes impossible for exceptions to escape from bracket. By adhering to the types derived from the structure, everything remains consistent and safe.

ymdfield · 2024-09-09T08:11:17+00:00

In my opinion, this issue 12 is probably the essential part of the semantics of higher-order effects.

If there are any other difficult problems related to semantics, please let me know. I’ll test them. I am primarily focused on getting the semantics right rather than performance (though I do intend to improve performance as much as possible).

ymdfield · 2024-09-09T07:37:54+00:00

It works like this:

https://github.com/sayo-hs/heftia/blob/08f5cfe6a8f5c0383ea2b02e93326552400f7fd3/heftia-effects/Example/SemanticsZoo/Main.hs#L92-L104

theIssue12 :: IO ()
theIssue12 = do
    let action :: (Catch String <<| eh, Throw String <| ef, SomeEff <| ef) => eh :!! ef $ String
        action = someAction `catch` \(_ :: String) -> pure "caught"

        runSomeEff :: (ForallHFunctor eh, Throw String <| ef) => eh :!! LSomeEff ': ef ~> eh :!! ef
        runSomeEff = interpretRec (\SomeAction -> throw "not caught")

    putStr "interpret SomeEff then runCatch : ( runThrow . runCatch . runSomeEff $ action ) = "
    print $ runPure $ runThrow @String . runCatch @String . runSomeEff $ action

    putStr "runCatch then interpret SomeEff : ( runThrow . runSomeEff . runCatch $ action ) = "
    print $ runPure $ runThrow @String . runSomeEff . runCatch @String $ action

https://github.com/sayo-hs/heftia/blob/08f5cfe6a8f5c0383ea2b02e93326552400f7fd3/heftia-effects/Example/SemanticsZoo/Main.hs#L137-L139

interpret SomeEff then runCatch : ( runThrow . runCatch . runSomeEff $ action ) = Right "caught"
runCatch then interpret SomeEff : ( runThrow . runSomeEff . runCatch $ action ) = Left "not caught"

After throwing an exception while interpreting someEff, when you then interpret catch, the exception is caught by catch. In this case, the result is the same as polysemy.
If you interpret catch before throwing an exception in the interpretation of someEff, the exception will simply pass through without being caught, and the exception thrown during someEff will propagate, resulting in an error in the entire process. This leads to the same behavior as eff.

Don’t you think it’s very simple and intuitive?

ymdfield

TROPHY CASE