Riyo

3 minute read

Part 1.1: Summary of Part 1 and an overview of heftia
Part 1.2: The performance and type safety of heftia
Part 1.3: Future prospects of heftia

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

Summary

heftia is the first-ever 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 Haskell effect library that aims to address major issues found in existing libraries:

  • Compatibility Problems with the UnliftIO

    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

  • Interoperability

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

    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.

Overview

heftia is a new effect system library for Haskell that I am currently developing. It uniquely provides fully realized implementations of algebraic and higher-order effects, 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

Recent advancements in research on algebraic effects have continued vigorously.

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. 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…

Comments

You May Also Enjoy