[ANN] A series of articles on Heftia: The Next Generation of Haskell Effects Management

Announcements
1

I have begun a series of articles on the next-generation effect library heftia and would like to make an announcement.

You can read the articles here:
Heftia: The Next Generation of Haskell Effects Management - Part 1.1

In the first installment, I covered:

  • Why use heftia instead of mtl or effectful
  • What kinds of challenges it addresses
  • Overview of the current Haskell effect ecosystem and future prospects

I would greatly appreciate your feedback!

heftia is the first effect library to fully support both algebraic and higher-order effects with complete type safety, high performance, and practical usability.

It solves long-standing issues in existing Haskell effect systems such as limitations of the IO monad approach, semantic unsoundness, and interoperability between libraries.

23 Likes
2

For people wanting a working example from the article for the instant gratification, I did it in a cabal script so you don’t have to (tested with GHC 9.10):

#!/usr/bin/env -S cabal run -v1
{- cabal:
build-depends: base, heftia
ghc-options: -Wall
-}
{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-missing-signatures #-}

import Prelude hiding (log, span)
import Control.Monad.Hefty

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

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

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

    log "bar"
4 Likes
3

The article says

effectful and bluefin have issues causing runtime errors if MonadUnliftIO, a typeclass intended for safe exception handling, is improperly used

Yet, these errors could be prevented at compile time by correctly designed interfaces, as heftia does. Exception safety should be guaranteed by types, not runtime checks.

But you don’t explain how heftia avoids the same problem. I see this instance:

 (UnliftIO :> es, Emb IO :> es, Monad (Eff ff es), Free c ff) => MonadUnliftIO (Eff ff es)

Could you elaborate why this is not subject to the same issues as effectful and Bluefin?

By the way, MonadUnliftIO isn’t “intended for safe exception handling”, nor is the problem experienced by effectful and Bluefin anything to do with “exception safety”.

3 Likes
4

You’re absolutely right. Let me explain it here.
(I hope to dive into the details from Part 2 onward; first I need to know whether people prefer an explanation of how to use it or of its internal mechanism…)

First, in effectful the Eff monad is always an instance of MonadUnliftIO. By contrast, in heftia UnliftIO is treated as a kind of higher-order effect, and only when UnliftIO :> es—that is, when UnliftIO appears in the effect list—does it become an instance of MonadUnliftIO. This distinction is the key to safety.

Let us consider file handles as an example of a resource. When defining a type-safe abstraction interface to guard against resource leaks (bluefin uses a different mechanism, I believe), effectful and polysemy employ the Provider a.k.a. Scoped higher-order effect.

In effectful, even if we use Provider, the following code that leaks the resource still compiles, and is only prevented at runtime:

import Effectful -- v2.5.1.0
import Effectful.Dispatch.Dynamic
import Effectful.FileSystem.IO
import Effectful.Provider
import System.IO (hPutStr)

data Write :: Effect where
    Write :: String -> Write m ()
type instance DispatchOf Write = Dynamic

write :: (Write :> es) => String -> Eff es ()
write = send . Write

runWriteIO
    :: (IOE :> es)
    => FilePath
    -> Eff (Write : es) a
    -> Eff es a
runWriteIO path m =
    runFileSystem $ withFile path WriteMode \h -> do
        interpret_ (\(Write s) -> liftIO $ hPutStr h s) (inject m)

main :: IO ()
main = do
    leakedAction :: IO () <- runEff do
        runProvider_ runWriteIO $ do
            provideWith_ @Write "out.txt" do
                withRunInIO \run -> pure $ run $ write "hi"

    leakedAction

-- > main
-- *** Exception: version (4) /= storageVersion (0)
-- If you're attempting to run an unlifting function outside of the scope of effects it captures, have a look at UnliftingStrategy (SeqForkUnlift).
-- CallStack (from HasCallStack):

In heftia, the type-safe resource abstraction is likewise performed via the Provider effect (more precisely, runRegionProvider). However, within the resource scope heftia prevents any use of the UnliftIO effect that could leak it. That is not to say UnliftIO is never available—only that it is only usable in ways that guarantee safety.

Hence, any attempt to leak a file handle is caught at compile time:

import Control.Monad.Hefty -- heftia-effects v0.7.0.0
import Control.Monad.Hefty.Provider
import Control.Monad.Hefty.Unlift
import Data.Functor.Identity
import System.IO (hPutStr)
import UnliftIO (IOMode (WriteMode), withFile)

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

type WriteProvider es = Provider Freer Identity FilePath '[Write] es

runWriteProvider
    :: (UnliftIO :> es, Emb IO :> es, Emb IO :> RemoveExps es, WeakenExps es)
    => Eff (WriteProvider (RemoveExps es) ': es) ~> Eff es
runWriteProvider =
    runRegionProvider_ @IO \path m -> do
        withFile path WriteMode \h ->
            m & interpret \case
                Write s -> liftIO $ hPutStr h s

main :: IO ()
main = do
    leakedAction :: IO () <- runUnliftIO do
        runWriteProvider $ do
            provide_ "out.txt" \_ ->do
                --      • The effect ‘UnliftBase IO’ does not exist within the effect list
                --          ‘[Write, Provider Freer Identity String '[Write] '[Emb IO],
                --            Emb IO]’
                --        Resolver: label
                --        Discriminator: UnliftBaseLabel IO
                --      • In a stmt of a 'do' block:
                --          withRunInIO \ run -> pure $ run $ write "hi"
                --        In the expression: do withRunInIO \ run -> pure $ run $ write "hi"
                --        In the second argument of ‘provide_’, namely
                --          ‘\ _ -> do withRunInIO \ run -> ...’
                --     |
                --     |                 withRunInIO \run -> pure $ run $ write "hi"
                --     |                 ^^^^^^^^^^^
                withRunInIO \run -> pure $ run $ write "hi"

    leakedAction

Ultimately, this is possible because heftia does not depend on the IO monad; instead it defines the Eff monad via a transparent Freer-style encoding of categorical objects, treating UnliftIO as just another higher-order effect rather than giving it special status.

According to the README.md of the unliftio:

Replace imports like Control.Exception with UnliftIO.Exception. Yay, your catch and finally are more powerful and safer (see Async exception safety)!

Of course, it may be true that MonadUnliftIO is not intended solely for safe exception handling, but it is clearly officially intended as one of its features. And I think the resource-leak examples so far relate to the functionality that guarantees exception safety of bracket, which relies on MonadUnliftIO in complex situations involving exceptions.

2 Likes
5

But in the examples of MonadUnliftIO allowing for escape in Bluefin and effectful the leaked action is run in Eff, not in IO. What happens if you run runUnliftIO at the top level, and run liftIO leakedAction within its scope?

6

Indeed, the codes did not fully match it…

Since runUnliftIO isn’t specifically involved in safety here, it yields the same result as follows:

main :: IO ()
main =
    runUnliftIO do
        leakedAction :: IO () <- runWriteProvider do
            provide_ "out.txt" \_ -> do
                --      • The effect ‘UnliftBase IO’ does not exist within the effect list
                --          ‘[Write, Provider Freer Identity String '[Write] '[Emb IO],
                --            Emb IO]’
                --        Resolver: label
                --        Discriminator: UnliftBaseLabel IO
                --      • In a stmt of a 'do' block:
                --          withRunInIO \ run -> pure $ run $ write "hi"
                --        In the expression: do withRunInIO \ run -> pure $ run $ write "hi"
                --        In the second argument of ‘provide_’, namely
                --          ‘\ _ -> do withRunInIO \ run -> ...’
                --     |
                --  40 |                 withRunInIO \run -> pure $ run $ write "hi"
                --     |                 ^^^^^^^^^^^
                withRunInIO \run -> pure $ run $ write "hi"

        liftIO leakedAction
2 Likes
7

Then I’m confused how you can use withRunInIO in Heftia’s Eff at all. Can you give an example of something non-trivial that’s not forbidden by the type system? For example, if instead of

withRunInIO \run -> pure $ run $ write "hi"

(which is bad, and correctly forbidden) suppose I want to use Control.Exception.catch in there? Can I? Surely Heftia forbids it regardless. I don’t see how it can distinguish a good use of Control.Exception.catch from a bad use of write "hi".

EDIT: I guess this comes down to

type FormOf (Emb e) = 'Polynomial

and

type FormOf (UnliftBase b) = 'Exponential

So UnliftIO is not available “inside” whereas Emb IO is. Is that right?

8

I attempted to use as many patterns as possible. throw, catch, withRunInIO, Provider, and so on:

import Control.Monad.Hefty (
    Eff,
    Effect,
    Emb,
    Freer,
    RemoveExps,
    UnliftIO,
    WeakenExps,
    interpret,
    liftIO,
    makeEffectF,
    (&),
    type (:>),
    type (~>),
 )
import Control.Monad.Hefty.Except (catch, runCatchIO, runThrowIO, throw)
import Control.Monad.Hefty.Provider (Provider, provide_, runRegionProvider_)
import Control.Monad.Hefty.Unlift (runUnliftIO, withRunInIO)
import Data.Functor.Identity (Identity)
import System.IO (hPutStr)
import UnliftIO (IOMode (WriteMode), withFile)

...

main :: IO ()
main =
    runUnliftIO do
        withRunInIO \run -> do
            run $ runWriteProvider do
                runThrowIO . runCatchIO $ do
                    catch
                        do
                            withRunInIO \run' -> do
                                run' $ withRunInIO \run'' -> do
                                    run'' $ provide_ "out.txt" \outer -> do
                                        write "hi"
                                        outer do
                                            withRunInIO \run''' -> do
                                                run''' $ throw $ userError "there"
                        \(e :: IOError) ->
                            withRunInIO \run' -> do
                                putStrLn "caught"
                                run' $ liftIO $ putStrLn $ "[ERROR] " <> show e

$ cabal run
caught
[ERROR] out.txt: withFile: user error (there)
$ cat out.txt
hi⏎

Yes, the ultimate criterion is whether the higher-order effect is a higher-order polynomial functor or an higher-order exponential functor with respect to resource protection.

This is somewhat technical, so I plan to explain it in a later article. Roughly speaking, when the structure of the effect exceeds a certain complexity, it can lead to resource leaks.

Polynomiality of higher-order functors is not covered in the Hefty Algebra paper (because the encoding employed in the paper can only encode polynomial effects), so one needs to research to other category theory literature… I have not yet thoroughly studied those. I would like to explain after understanding them.

However, we don’t need to understand these when using it. We simply check the types of the functions in Haddock or, via HLS’s mouse hover, whether UnliftIO is included in the effect list. If it is, we can use it; if it isn’t, we cannot.

It depends on what is meant by inside…

9

In the scope of the runWriteProvider.

Would you mind adding explicit imports so I can see where everything is coming from (particularly throw and catch, where it is not lexically obvious whether they are from Control.Exception or from Heftia)?

1 Like
10

Understood. As shown in the code, it is usable; the unusable parts are specific sections within provide_.

Certainly, I have edited it.

1 Like
11

I see. Given the type of provide_ I don’t think I’ll be able to understand how that works!

provide_ :: forall i a (es' :: [Effect]) (es :: [Effect]) (r :: [Effect]) (ff :: (Type -> Type) -> Type -> Type) (c :: (Type -> Type) -> Constraint). (Provider ff Identity i es r :> es', forall (es'' :: [Effect]). Functor (Eff ff es''), Free c ff) => i -> ((Eff ff es' ~> Eff ff (es ++ (Provider ff Identity i es r ': r))) -> Eff ff (es ++ (Provider ff Identity i es r ': r)) a) -> Eff ff es' a

Thanks. Really I was looking for an example of using MonadUnliftIO with a “standard” higher order effect such as Control.Exception.catch or Control.Exception.bracket. EDIT: For example, to bracket an operation whose body contains write "hi".

1 Like
12

Ah, I see? (BTW I don’t think Control.Exception.catch or Control.Exception.bracket are higher-order effects… They’re tied to the semantics of IO, and their behavior isn’t interpreted by a handler or anything like that…)

If you could provide pseudocode or something written in a style closer to libraries like effectful, it would be easier to answer.

13

Unfortunately I can’t get the code to compile with hefia-0.7.0.0 on GHC 9.6 or 9.10. Could you please include complete working source code for an example, including language extensions?

Yes, I’m talking about something like the following (which runs with cabal repl -z -b bluefin==0.0.15.0):

import Bluefin.Eff (runEff_)
import Bluefin.IO (withEffToIO_)
import Bluefin.System.IO (hPutStrLn, withFile)
import System.IO (IOMode (WriteMode))
import Control.Exception

main = runEff_ $ \io -> do
  withFile io "/tmp/out" WriteMode $ \h -> do
    withEffToIO_ io $ \effToIO -> do
      bracket
        (putStrLn "Acquiring resource")
        (\() -> putStrLn "Releasing resource")
        (\() -> effToIO (hPutStrLn h "Hello"))
14

The Haddock output from the current configuration isn’t very good (I’ll try to improve it). The kind isn’t necessary for display, and aside from that, it’s not actually that complicated.

Just like with the type of lens, we’ll need appropriate type synonyms going forward. After all, lens types are probably about this complex when fully expanded.

In terms of complexity, it’s cruel to leave criteria that really require this level of type-level protection to careful human attention rather than having the compiler enforce them.

I created a cabal script in GHC 9.8.4.

I’ll get some sleep first, and then I’ll give it a try. Thanks for the code.

2 Likes
15

This code is what I think you “should” be able to write with Heftia, but there’s a type error, because UnliftIO is not available.

Code 
#!/usr/bin/env -S cabal run -v1
{- cabal:
build-depends: base, heftia-effects ^>= 0.7, unliftio
ghc-options: -Wall
-}
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}

import Control.Monad.Hefty
  ( Eff,
    Effect,
    Emb,
    Freer,
    RemoveExps,
    UnliftIO,
    WeakenExps,
    interpret,
    liftIO,
    makeEffectF,
    (&),
    type (:>),
    type (~>),
  )
import Control.Exception (bracket)
import Control.Monad.Hefty.Provider (Provider, provide_, runRegionProvider_)
import Control.Monad.Hefty.Unlift (runUnliftIO, withRunInIO)
import Data.Functor.Identity (Identity)
import System.IO (hPutStr)
import UnliftIO (IOMode (WriteMode), withFile)

data Write :: Effect where
  Write :: String -> Write f ()

makeEffectF ''Write

type WriteProvider es = Provider Freer Identity FilePath '[Write] es

runWriteProvider ::
  (UnliftIO :> es, Emb IO :> es, Emb IO :> RemoveExps es, WeakenExps es) =>
  Eff (WriteProvider (RemoveExps es) ': es) ~> Eff es
runWriteProvider =
  runRegionProvider_ @IO \path m -> do
    withFile path WriteMode \h ->
      m & interpret \case
        Write s -> liftIO $ hPutStr h s

main :: IO ()
main =
  runUnliftIO do
    runWriteProvider do
      provide_ "out.txt" \_ -> do
        withRunInIO \run -> do
            bracket
              (putStrLn "Acquiring resource")
              (\() -> putStrLn "Releasing resource")
              (\() -> run (write "hi"))

Thanks and sleep well.

1 Like
16

Compared to effectful, currently the fastest among practical libraries, heftia is only slightly slower.

effectful: 2.18ms, heftia: 3.10ms. That’s a 42% difference.

In fact, other benchmarks show that in some cases (such as using Throw/Catch effects with Except), heftia even outperforms effectful.

effectful uses runtime exceptions underneath for errors. From skimming the source code heftia doesn’t. How well does it work with the ubiquitous exceptions library? If it doesn’t (which in itself is a problem), where is the bracket function?

Also, you didn’t mention that performance of effectful doesn’t depend on the amount of effects on the stack, while heftia slows down with each effect added (shallow vs deep stack).

One significant reason, identified in the paper “Reflection without Remorse,” can be resolved by using a data structure called FTCQueue, enabling performance comparable to effectful. :right_arrow_curving_left:

Why is heftia not using it then? :thinking:

I admire your persistence in trying to make this work, but my opinion remains the same: turning all code into data with free monads is a horrendous idea. As an example, select polysemy users have run into mysterious space leaks which remain unsolved and it’s not at all clear other free-monad based implementations won’t suffer from unexpected performance issues at scale.

IO monad-based libraries like effectful, cleff, and bluefin continually discover and patch issues, as seen in GitHub issues

First of all, “continually” is a baseless exaggeration. Bluefin doesn’t seem to have any bug reports in its issue tracker and looking at effectful’s issue tracker, there are few bug reports (most are questions or feature requests), the last of which was fixed over 6 months ago. Second, this whole sentence makes for a real WTF moment. “Look, these other libraries that were around for quite a while and people are using in production HAD BUGS!” This almost reads like you think your library won’t have bugs, because it’s based on a paper. Well…

On the other hand, heftia directly implements categorical foundations described in academic papers

Wasn’t polysemy also based on a paper?

However, “the Haskell way” offers a superior approach. By consistently translating mathematical concepts into Haskell code using algebraic data types, encoding categorical constructs through types, equational reasoning, and parametricity, we can guarantee from the outset the absence of various classes of bugs.

I firmly believe maintaining this method is critical for the future of Haskell’s effect system. Establishing theoretically sound interfaces helps prevent repeated costly migrations. heftia is intended as practical proof of this methodology.

Now we need to wait a few years to see how well this statement ages :slight_smile:

4 Likes
17

Edit: Although I initially wrote a reply here, I realized that it is more important to revise the expressions in the article that may still lead to misunderstandings, and, if necessary, to incorporate the content of the reply into the article itself. I would appreciate any ideas on how best to make these revisions.

My current thinking is that the correct approach to constructive discussion would be to remove all parts that imply practicality or a comparison of “superiority or inferiority” with other effect libraries, and instead rewrite the articles purely as a presentation of ideas. What do you think?

1 Like
18

I acknowledge that the article contained many value judgments based on my personal design philosophy. I apologize for having published such an inadequate piece. I have now reposted a revised version with those elements removed as much as possible.

If you would be willing to review it and check whether it contains any content that hinders constructive discussion, I would greatly appreciate it.

3 Likes
19

It is using it.

I am not claiming heftia is free of bug, but as long as there are no bugs in GHC itself, we can guarantee that runtime errors do not occur outside the part of the implementation using unsafe for extensible sums. This is because those parts simply do not include logic that could cause runtime errors in the first place. The extensible sum portion, unlike the entire effect system, has a simple structure and is theoretically settled, so automated tests work effectively.

Furthermore, the operational semantics defined in the paper can also be mathematically proven to match the behavior of functions using type isomorphisms and equational reasoning. This has not been done yet, as I am prioritizing practical improvements, but I plan to start working on it once the first bug report related to semantics arrives in the issue tracker.

Under this guarantee of type safety, we can also extend this assurance to the surrounding ecosystem (so long as they do not use unsafeCoerce etc.), ensuring that certain types of bugs (runtime errors) will not occur.

I believe that such characteristics are not commonly seen, at least in the ReaderT IO approach. What is your view on this?

It adopted an ad-hoc mechanism called “Weaving,” which did not rely on category theory or any well-defined semantics. The point is not that it was a paper but that it had a clearly defined underlying mathematical theory and formal correspondence.

6 Likes
20

Now that I have had the chance to read the article more closely I can point out a number of claims that do not match my understanding.

Problems with the IO Monad approach: Potential lack of type safety

No justification is given for this claim. If there is an actual lack of type safety an example should be given. I’m not sure what “potential” could mean here, but if you think it’s likely that IO-wrapper effect systems are vulnerable to undiscovered type safety issues than I that that warrants a couple of sentences of explanation.

Fundamental inability to support algebraic effects (delimited continuations) due to reliance on MonadUnliftIO

Indeed IO-wrapper effect systems do not support multishot continuations, but that has nothing to do with MonadUnliftIO, it’s simply because IO doesn’t. I also think this warrants a sentence or two explaining why anyone should care about multishot continuations. I think this is far from settled understanding, and my request for a compelling example of LogicT on Twitter went unanswered.

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

Ultimately all IO-wrapper effect systems are compatible, exactly because they are based on IO. There hasn’t been much work making them practically compatible, but I don’t envisage much difficulty here.

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.

I think it’s worth a sentence or two defining “algebraic effects”. I, for one, still don’t know what “algebraic effect” means (or even if it’s a formal or informal concept).

effectful and bluefin have issues causing runtime errors if MonadUnliftIO, a typeclass intended for safe exception handling, is improperly used

That doesn’t really get to the heart of the matter. MonadUnliftIO is unsafe full stop for effect tracking systems that expose its full functionality. It seems that Heftia gets around this by not exposing its full functionality. That’s fair enough! But it’s still unclear whether Heftia supports enough of its functionality to justly claim it supports it at all.

The methodology behind the IO monad approach involves iterative experimentation—implementing solutions, encountering issues, and then applying ad-hoc patches … This leads to a constant cycle of discovering and patching new issues. Such a methodology becomes increasingly risky near the core of an ecosystem. A foundational issue discovered later could necessitate interface changes so extensive that they would break compatibility across the ecosystem.

Has the author been involved in the design and implementation of an IO-wrapper effect system to be able to make claims what its methodology involved? The description here certainly doesn’t match the methodology of Bluefin. Bluefin is based on the ST approach which has robust theory behind it. There has been no cycle of discovering and patching new issues, and given the pre-existing theory it seems unlikely that any such foundational issue will be discovered.

IO monad-based libraries like effectful, cleff, and bluefin continually discover and patch issues, as seen in GitHub issues

This claim does not match my understanding and I think the author would do well to provide some evidence, such as links to GitHub issues if he wants to make claims like this. Certainly I would not describe my experience developing Bluefin as one of “continually discovering and patching issues”.

Please consider building an ecosystem robust to future theoretical developments, encouraging mutual interoperability, such as the data-effects approach advocated by heftia.

I fear the author may have fallen into the “N+1 competing standards trap” explained by XKCD.

Let us stop repeating the cycle of migration hell.

It’s not clear that IO-based effect systems suffer from migration hell.

Let us work together to build the future of the Haskell effect system ecosystem.

I’m happy to collaborate to improve the effect system ecosystem, if there’s something beneficial I can do on the Bluefin side.

2 Likes