Riyo

4 minute read

This article has been revised. The revised article is: /blog/heftia/heftia-rev-part-1-1/

Part 1.1: Summary of Part 1 and an overview of heftia
Part 1.2: The performance of heftia
Part 1.3: Issues with the increasingly popular IO monad approach
Part 1.4: Future prospects of heftia

In this series, I will explain heftia. This is the first part.

Summary

heftia is the first-ever fully type-safe and performant effect system, not just among Haskell libraries but historically across all effect system implementations and languages, to completely implement both algebraic effects and higher-order effects.

GitHub - sayo-hs/heftia: A theory‑backed, ultra type‑safe algebraic effects

GitHub - sayo-hs/heftia: A theory‑backed, ultra type‑safe algebraic effects

A theory‑backed, ultra type‑safe algebraic effects - sayo-hs/heftia

heftia is a next-generation Haskell effect library that addresses major issues in current libraries through a unified solution:

  • Problems with the IO Monad approach

    Issues inherent to the IO monad (ReaderT IO) approach employed by libraries such as effectful, cleff, and bluefin:

    • Potential lack of type safety
    • Fundamental inability to support algebraic effects (delimited continuations) due to reliance on MonadUnliftIO

  • Semantic Soundness

    Unsound semantics that occur when combining higher-order effects with algebraic effects (delimited continuations) in effect libraries predating effectful, such as polysemy, fused-effects, and freer-simple

  • Interoperability

    Fragmentation of the Haskell ecosystem and significant migration costs due to the proliferation of incompatible effect libraries

Overview

heftia is a new effect system library for Haskell that I am currently developing. It uniquely provides practical, fully realized implementations of algebraic and higher-order effects with performance suitable for real-world use, unmatched by any other existing effect system or language.

  • Higher-order effects are effects that take monadic actions as arguments. In terms of monad transformers, examples include local in ReaderT and catch in ExceptT. In contrast, operations like put/get in StateT, ask in ReaderT, and throw in ExceptT are classified as first-order effects.

    Without higher-order effects, it becomes difficult to use functions like local or catch flexibly, which can be quite inconvenient.

  • Algebraic effects are a programming paradigm that has gained attention in recent years. They are a language feature and theoretical framework aimed at improving composability and maintainability of programs.

    They have applications in areas such as coroutines and concurrent programming, offering a unified way to express and use such constructs. Algebraic effects extend existing control structures, allowing various kinds of control flows—like lightweight threads, asynchronous I/O, or exception handling—to be modularized safely and switched dynamically in a predictable manner.

    Roughly speaking, they overcome the limitations of monad transformers, offering a more convenient, safer, and more predictable alternative.

Here is a comparison table of heftia and other effect system implementations in terms of their features:

Library or Language Higher-Order Effects Algebraic Effects (Delimited Conts)
heftia ✅ ✅
mtl ⚠️ ⚠️
effectful ✅ ❌
bluefin ✅ ❌
polysemy ✅ ❌
fused-effects ✅ ❌
eff ⚠️ ✅
freer-simple ❌ ✅
in-other-words ✅ ⚠️
speff ⚠️ ✅
Koka-lang ❌ ✅
Eff-lang ❌ ✅
OCaml-lang 5 ❌ ✅

✅ = Fully supported / sound
⚠️ = Partially supported or with semantic issues
❌ = Not supported

As shown, heftia is the only implementation that combines all of these features.

Over time, numerous Haskell effect libraries have been released, encountered problems, and been replaced by newer solutions. Libraries such as fused-effects, polysemy, and more recently cleff, effectful, and bluefin, have all emerged.

Due to incompatibility among these libraries, migrating between them has incurred significant costs. Today, the community seeks a definitive solution that ends the cycle of migration hell.

Recently, the IO monad approach (ReaderT IO) exemplified by effectful has attracted attention as the closest thing to such a definitive solution. It has been praised for improved performance and practical usability compared to previous approaches (mtl or Freer-based methods), albeit by sacrificing support for algebraic effects (delimited continuations).

You no longer have to sacrifice support for algebraic effects just to get high performance. Recent advancements in research on algebraic effects have continued vigorously.

Leveraging recent solid theoretical foundations1, heftia simultaneously provides algebraic effect capabilities and high performance, along with ultimate type safety, practicality, and enduring interoperability with other effect libraries.

Code Example

In addition to Hackage, it is also currently available on Stackage Nightly. Usage is explained on Haddock.

The following is an example of defining, using, and interpreting the first-order effect Log for logging and the higher-order effect Span for representing named spans in a program.

data Log :: Effect where
    Log :: String -> Log f ()
makeEffectF ''Log

data Span :: Effect where
    Span :: String -> f a -> Span f a
makeEffectH ''Span

runLog :: (Emb IO :> es) => Eff (Log : es) ~> Eff es
runLog = interpret \(Log msg) -> liftIO $ putStrLn $ "[LOG] " <> msg

runSpan :: (Emb IO :> es) => Eff (Span : es) ~> Eff es
runSpan = interpret \(Span name m) -> do
    liftIO $ putStrLn $ "[Start span '" <> name <> "']"
    r <- m
    liftIO $ putStrLn $ "[End span '" <> name <> "']"
    pure r

prog :: IO ()
prog = runEff . runLog . runSpan $ do
    span "example program" do
        log "foo"

        span "greeting" do
            log "hello"
            log "world"

        log "bar"

> prog
[Start span 'example program']
[LOG] foo
[Start span 'greeting']
[LOG] hello
[LOG] world
[End span 'greeting']
[LOG] bar
[End span 'example program']

As you can see, the interface is similar to that of effectful or polysemy, and is very concise.

Type inference for effects works without the need for any special GHC plugins. When using put/get of State, there’s no need to explicitly specify types like @Int or ... :: Int.

To be continued in Part 1.2…

  1. Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects. Casper Bach Poulsen & Cas van der Rest, POPL 2023.
    A Framework for Higher-Order Effects & Handlers. Birthe van den Berg & Tom Schrijvers, Sci. Comput. Program. 2024. ↩

Comments

You May Also Enjoy