Heftia

Heftia is a higher-order effects version of Freer.

The paper

• Casper Bach Poulsen and Cas van der Rest. 2023. Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects. Proc. ACM Program. Lang. 7, POPL, Article 62 (January 2023), 31 pages. https://doi.org/10.1145/3571255

inspires this library. Hefty trees, proposed by the above paper, are extensions of free monads, allowing for a straightforward treatment of higher-order effects.

This library offers Heftia monads and Freer monads, encoded into data types in several ways to enable tuning in pursuit of high performance.

Status

Please note that this library is currently in the experimental stage. There may be significant changes and potential bugs.

Example

Compared to existing Effect System libraries in Haskell that handle higher-order effects, this library's approach allows for a more effortless and flexible handling of higher-order effects. Here are some examples:

• Extracting Multi-shot Delimited Continuations

  In handling higher-order effects, it's easy to work with multi-shot delimited continuations. This enables an almost complete emulation of "Algebraic Effects and Handlers". For more details, please refer to the example code.

• Two interpretations of the censor effect for Writer

  Let's consider the following Writer effectful program:

  hello :: (Tell String <: m, Monad m) => m ()
  hello = do
      tell "Hello"
      tell " world!"
  
  censorHello :: (Tell String <: m, WriterH String <<: m, Monad m) => m ()
  censorHello =
      censor
          ( \s ->
              if s == "Hello" then
                  "Goodbye"
              else if s == "Hello world!" then
                  "Hello world!!"
              else
                  s
          )
          hello
  

  For censorHello, should the final written string be "Goodbye world!" (Pre-applying behavior) ? Or should it be "Hello world!!" (Post-applying behavior) ? With Heftia, you can freely choose either behavior depending on which higher-order effect interpreter (which we call an elaborator) you use.

  main :: IO ()
  main = runEff do
      (sPre, _) <-
          interpretTell
              . interpretH (elaborateWriterPre @String)
              $ censorHello
  
      (sPost, _) <-
          interpretTell
              . interpretH (elaborateWriterPost @String)
              $ censorHello
  
      sendIns $ putStrLn $ "Pre-applying: " <> sPre
      sendIns $ putStrLn $ "Post-applying: " <> sPost
  

  Using the elaborateWriterPre elaborator, you'll get "Goodbye world!", whereas with the elaborateWriterPost elaborator, you'll get "Hello world!!".

  Pre-applying: Goodbye world!
  Post-applying: Hello world!!
  

  For more details, please refer to the complete code and the implementation of the elaborator.

Furthermore, the structure of Heftia is theoretically straightforward, with ad-hoc elements being eliminated.

Heftia is the current main focus of the Sayo Project.

Documentation

The example codes are located in the heftia-effects/Example/ directory.

Examples with explanations can be found in the docs/examples/ directory. Documents have become outdated. Please wait for the documentation for the new version to be written.

Future Plans

• Benchmarking

• Enriching the documentation

• Completing missing definitions such as

  • handlers for the Accum, Coroutine, Fresh, Input, Output effect classes

  and others.

License

The license is MPL 2.0. Please refer to the NOTICE. Additionally, this README.md and the documents under the docs/docs-ja directory are licensed under CC BY-SA 4.0.

Your contributions are welcome!

Please see CONTRIBUTING.md.

Credits

Parts of this project have been inspired by the following resources:

• Hefty Algebras -- The Artifact
  • Copyright (c) 2023 Casper Bach Poulsen and Cas van der Rest
  • License: MIT