[ANN] heftia-effects: higher-order algebraic effects done right

Announcements
#1

I’m excited to announce heftia-effects, a new extensible effects library for Haskell.

Key Features

  • Correct Semantics for Higher-Order Effects & Continuations

    Heftia provides the following features simultaneously, which existing libraries could not support together:

    • Higher-order effects
    • Delimited continuations (algebraic effects)
      • Coroutines (non-scoped resumptions)
      • Non-deterministic computations
    • MonadUnliftIO

    All of these interact through a simple, consistent, and predictable semantics based on algebraic effects.

  • Easy and Concise Implementation for Custom Effect Interpreters

    As you can see from the implementations of basic effect interpreters such as State, Throw/Catch, Writer, NonDet, and Coroutine, they can be implemented in just a few lines, or even a single line. Even for effects like NonDet and Coroutine, which involve continuations and might seem difficult to implement at first glance, this is exactly how simple it can be. This is the power of algebraic effects. Users can quickly define experimental and innovative custom effects using continuations.

  • Standard and Reasonable Performance

    It operates at a speed positioned roughly in the middle between faster libraries (like effectful or eveff) and relatively slower ones (like polysemy or fused-effects): performance.md.

  • Purity

    • Does not depend on the IO monad and can use any monad as the base monad.
    • Semantics are isolated from the IO monad, meaning that aspects like asynchronous exceptions and threads do not affect the behavior of effects.

If you’re interested, please take a look at the documentation for usage and semantics.
I’d love to hear your thoughts!

There are countless effect system libraries in Haskell, so to be honest, I was unsure whether to announce this library. However, after several updates, I believe that Heftia v0.4 now offers value comparable to other major effect system libraries. The current version is no longer experimental and aims to provide a practical effect system.

More Details

Background

Traditional libraries have always struggled with semantic issues in higher-order effects*1*2*3*4.
Heftia is based on algebraic effects and provides a simple, consistent, and predictable semantics for all interactions of effects, thereby providing answers to these issues comprehensively.

Effect and its interpreter designers only need to consider the semantics of algebraic effects and do not need to worry about the library’s internal implementation or IO monad-level details*5.

This significantly simplifies the process of creating custom effects and writing their interpreters.
Type safety ensures that there is no concern about breaking semantics, allowing users to focus solely on the inherent complexity of their tasks.

Robustness of Semantics

This library prevents inherently dangerous operations*6 that could break or obscure semantics through type safety.

This is not something added in an ad-hoc manner through methods like smart constructors but is naturally derived from the straightforward data structure of the Eff monad.

The constructors of the Eff monad are exposed, and users can manipulate them directly without any safety concerns, yet the semantics remain intact.

Performance

This library is based on the Freer monad, which is somewhat traditional, rather than using the recent mainstream approaches like evidence passing (ReaderT IO pattern) used by effectful, cleff, or bluefin*7. It’s not extremely fast, but it’s built on the fast implementation freer-simple, resulting in a speed that is positioned roughly in the middle between the high-speed IO-based implementations and relatively slower implementations. In typical usage, you should find the performance satisfactory.

Additionally, by basing on Freer, the semantics of the effect system are separated from the semantics of IO. This means that when interpreting effects, there is no need to consider IO-level details*5. The consistent semantics of algebraic effects prevent leaky abstraction from the IO level. This is a significant difference from IO-fused effect system libraries like effectful and cleff, and it’s one of the reasons why this library is based on Freer rather than on IO.

*1: The effect semantics zoo - lexi-lambda/eff
*2: Incorrect semantics for higher-order effects - hasura/eff#12
*3: Semantics of higher order effects - re-xyr/speff#3
*4: Unresolved challenges of scoped effects
*5: Examples include “Asynchronous exceptions might be thrown,” “What is the current state of exception masking,” “This state/environment value is local and thus not shared between threads,” and more.
*6: For instance, interpreting the coroutine effect while the catch effect is still uninterpreted and interpreting the catch effect afterwards.
*7: In particular, Heftia doesn’t use GHC’s delimited continuation primops.

17 Likes
#2

Thanks for creating this! You mentioned that it’s inspired by this paper.

How does it relate to Nicholas Wu’s work as mentioned in The Evolution of Effects (Haskell 2023) - ICFP 2023? It seems ICFP has been full of research on algebraic effects lately and I’m trying to see where this fits in.

1 Like
#3

What’s the reason for avoiding GHC’s delimited continuation primops? Are they necessarily tied to using IO as an underlying mechanism?

1 Like
#4

Actually, the delimited-continuation primitives proposed for GHC don’t rely on IO a :

type PromptTag# (a :: Type)

newPromptTag# 
  :: forall (a :: Type). State# RealWorld
  -> (State# RealWorld, PromptTag a)

prompt#
  :: forall (a :: Type)
   . PromptTag# a
  -> (State# RealWorld -> (# State# RealWorld, a #))
  -> State# RealWorld -> (# State# RealWorld, a #)

control0#
  :: forall (a :: Type) (r :: RuntimeRep) (b :: TYPE r)
   . PromptTag# a
  -> (((State# RealWorld -> (# State# RealWorld, b #))
       -> State# RealWorld -> (# State# RealWorld, a #))
      -> State# RealWorld -> (# State# RealWorld, a #))
  -> State# RealWorld -> (# State# RealWorld, b #)

Moreover, the author explicitly warns against using them as operations for IO a :

…which seems as good a reason as any to avoid their use (assuming there’s been no changes beyond what was originally proposed).

1 Like
#5

Isn’t IO just a type synonym for State# RealWorld?

1 Like
#6

I’m sorry if I interrupted the discussion.

Essentially, yes. The reason is that GHC’s delimited continuation primops require the IO monad to execute them. In my design approach, libraries like fused-effects, polysemy, and freer-simple allow using any monad as the base monad. This isolates the semantics from the IO level, preventing users from falling into pitfalls caused by leaky abstractions from the IO layer. Relying on the IO monad would eliminate this property, which is a major concern for me.

Additionally, the situation is somewhat more complex and relates to the actual performance of primops. Benchmark results for the eff library, which utilizes primops for optimization, raise questions about the true speed benefits of primops. Specifically, effects like NonDet and Coroutine exhibit O(n²) level slowness. However, this may be due to the implementation of eff rather than the primops themselves.

During the performance improvement process for Heftia, I first forked a library called speff to prototype an IO-based version of Heftia (which also does not use primops). 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.

Therefore, I changed my approach and optimized based on Freer using freer-simple, achieving practical speeds. This demonstrated that not only for semantic reasons but also for performance compatibility, Freer was a better fit. Consequently, Freer was adopted.

5 Likes
#7

No. For GHC, it’s:

Also see How to Declare an Imperative for other pedagogical implementations of IO a.

2 Likes
#8

To be honest, I hadn’t been able to keep up with these developments much, but the primitives are provided under the assumption that programmers understand they are unsafe and will wrap them with invariant-preserving wrappers (such as libraries like eff). While IO is indeed merely a newtype around State#, it is specifically wrapped in a newtype intended to allow users to call it safely without any particular prior knowledge. Therefore, it’s understandable that such safe wrappers are not provided.

It appears that IO versions of prompt and control0 (those without the #) have not been provided, consistent with the proposal without any changes.

#9

Are you referring to work around 2015, such as “Effect Handlers in Scope” or “Fusion for Free,” which underpin the fused-effects library?

#10

Yes, “Effect Handlers in Scope”, but also more recent work from 2023: “A Framework for Higher-Order Effects and Handlers” (not Wu’s work, but cited) and “Modular Models of Monoids with Operations”.

2 Likes
#11

OK. It seems that around 2015, the so-called “higher-order free monad” hadn’t been developed, so the standard first-order free monad was used instead. The approach to higher-order effects differs from Hefty Algebras and the A Framework for Higher-Order Effects & Handlers (2023), which are based on the higher-order free monad.

Specifically, fused-effects cannot encode coroutine effects and is aligned with “functorial state” semantics (similar to polysemy). In contrast, my library follows the continuation-based lineage of freer-simple and eff, resulting in a different approach.

I believe my library is closely aligned with “A Framework for Higher-Order Effects & Handlers,” as the Eff monad in my library corresponds to the higher-order free monad defined in that paper (p7). The higher-order functors K^Par for concurrency that appear in the paper (pp. 14-15) can be defined in this library as the exact same GADTs presented in the paper and used as higher-order effects:

data KPar rho f a where
    For :: rho (f b) -> (rho b -> a) -> KPar rho f a

In this sense, structurally, the framework in this paper is almost equivalent (although the concept of elaboration does not appear in the paper, and only a brief mention of Hefty Algebras is made towards the end).

Regarding “Modular Models of Monoids with Operations,” I have glanced through it, but I’m sorry, it was difficult for me to read due to the extensive use of category theory. The categorical foundation of algebraic effects is currently beyond my understanding.

I hope this is helpful.

3 Likes
#12

That was very helpful, thanks! I was encouraged by Nicholas Wu’s 2023 talk and the work on higher-order effects, and it sounds like your library incorporates the same idea.

1 Like