search

sayo-hs / heftia

higher-order effects done right for Haskell
Mozilla Public License 2.0
46 stars 1 forks source link

readme

Heftia: higher-order effects done right for Haskell

Hackage Hackage

Heftia is a higher-order effects version of Freer.

This library provides "continuation-based semantics" for higher-order effects, the same as lexi-lambda's eff. Instead of using the IO monad to implement delimited continuations for effects, Heftia internally uses Freer monad.

The paper

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 Hefty monads and Freer monads, encoded into data types in several ways to enable tuning in pursuit of high performance.

Status

This library is currently in the beta stage. There may be significant changes and potential bugs.

Specifically, significant performance improvements are required: https://github.com/sayo-hs/heftia/issues/12

We are looking forward to your feedback!

Installation

1.

    $ cabal update

  1. Add heftia-effects ^>= 0.3.1 and ghc-typelits-knownnat ^>= 0.7 to the build dependencies. Enable the ghc-typelits-knownnat plugin, GHC2021, and the following language extensions as needed:

    • LambdaCase
    • DerivingStrategies
    • DataKinds
    • TypeFamilies
    • BlockArguments
    • FunctionalDependencies
    • RecordWildCards
    • DefaultSignatures
    • PatternSynonyms

Example .cabal:

...
    build-depends:
        ...
        heftia-effects ^>= 0.3.1,
        ghc-typelits-knownnat ^>= 0.7,

    default-language: GHC2021

    default-extensions:
        ...
        LambdaCase,
        DerivingStrategies,
        DataKinds,
        TypeFamilies,
        BlockArguments,
        FunctionalDependencies,
        RecordWildCards,
        DefaultSignatures,
        PatternSynonyms,
        TemplateHaskell,
        PartialTypeSignatures,
        AllowAmbiguousTypes

    ghc-options: ... -fplugin GHC.TypeLits.KnownNat.Solver
...

This library has been tested to work with GHC 9.2.8. Versions of base 4.17 and later (GHC 9.4.1 and later) are not currently supported. Please wait for an update. https://github.com/sayo-hs/heftia/issues/11#issue-2509400153

Getting Started

To run the SemanticsZoo example:

$ git clone https://github.com/sayo-hs/heftia
$ cd heftia/heftia-effects
$ cabal run exe:SemanticsZoo
...
# State + Except
( evalState . runThrow . runCatch $ action ) = Right True
( runThrow . evalState . runCatch $ action ) = Right True

# NonDet + Except
( runNonDet . runThrow . runCatch . runChooseH $ action1 ) = [Right True,Right False]
( runThrow . runNonDet . runCatch . runChooseH $ action1 ) = Right [True,False]
( runNonDet . runThrow . runCatch . runChooseH $ action2 ) = [Right False,Right True]
( runThrow . runNonDet . runCatch . runChooseH $ action2 ) = Right [False,True]

# NonDet + Writer
( runNonDet . runTell . elaborateWriter . runChooseH $ action ) = [(3,(3,True)),(4,(4,False))]
( runTell . runNonDet . elaborateWriter . runChooseH $ action ) = (6,[(3,True),(4,False)])

# https://github.com/hasura/eff/issues/12
interpret SomeEff then runCatch : ( runThrow . runCatch . runSomeEff $ action ) = Right "caught"
runCatch then interpret SomeEff : ( runThrow . runSomeEff . runCatch $ action ) = Left "not caught"

[Note] All other permutations will cause type errors.
$

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, _) <-
        runTell
            . interpretRecH (elabWriterPre @String)
            $ censorHello

    (sPost, _) <-
        runTell
            . interpretRecH (elabWriterPost @String)
            $ censorHello

    liftIO $ putStrLn $ "Pre-applying: " <> sPre
    liftIO $ putStrLn $ "Post-applying: " <> sPost

Using the elabWriterPre elaborator, you'll get "Goodbye world!", whereas with the elabWriterPost 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.

Additionally, Heftia supports not only monadic effectful programs but also applicative effectful programs. This may be useful when writing concurrent effectful code.

Heftia is the current main focus of the Sayo Project.

Documentation

The example codes are located in the heftia-effects/Example/ directory. Also, the following HeftWorld example: https://github.com/sayo-hs/HeftWorld

About the internal mechanism: https://sayo-hs.github.io/jekyll/update/2024/09/04/how-the-heftia-extensible-effects-library-works.html

Examples with explanations in Japanese can be found in the docs-ja/examples/ directory.

Comparison

Library or Language Higher-Order Effects Delimited Continuation Effect System Purely Monadic Dynamic Effect Rewriting Semantics Performance
Heftia Yes Multi-shot Yes Yes (also Applicative and others) Yes continuation-based ^5
freer-simple No Multi-shot Yes Yes Yes continuation-based ?
Polysemy Yes No Yes Yes Yes weaving-based (functorial state) ?
Effectful Yes No Yes No (based on the IO monad) Yes IO-fused ?
eff Yes Multi-shot Yes No (based on the IO monad) Yes continuation-based & IO-fused ^6 ?
speff Yes Multi-shot (restriction: [^4]) Yes No (based on the IO monad) Yes continuation-based & IO-fused ?
in-other-words Yes Multi-shot? Yes Yes No? carrier dependent ?
mtl Yes Multi-shot (ContT) Yes Yes No carrier dependent ?
fused-effects Yes No? Yes Yes No carrier dependent & weaving-based (functorial state) ?
koka-lang No ^2 Multi-shot Yes No (language built-in) Yes continuation-based ?
OCaml-lang 5 ? One-shot No [^3] No (language built-in) ? continuation-based? ?

[^3]: Effects do not appear in the type signature and can potentially cause unhandled errors at runtime [^4]: Scoped Resumption only. e.g. Coroutines are not supported.

Heftia can simply be described as a higher-order version of freer-simple. This is indeed true in terms of its internal mechanisms as well.

Additionally, this library provides a consistent continuation-based semantics that is independent of carriers and effects. On the other hand, in libraries like in-other-words, mtl, and fused-effects, the semantics of the code depend on the effect and, in part, the carrier inferred by type inference. Fixing the semantics to a continuation-based model helps improve the predictability of the behavior (interpretation result) of the code.

Carrier-dependent semantics can lead to unexpected behavior for code readers, particularly in situations where the types become implicit. Particularly, attention should be given to the fact that due to type inference, semantic changes may propagate beyond the blocks enclosed by interpret or interpose. In the case of carrier-independent semantics, especially with Freer-based effects, interpret and interpose do not alter the semantics by intervening in type inference or instance resolution of the carrier. Instead, they function as traditional functions, simply transforming the content of the data structure. This results in minimal surprise to the mental model of the code reader.

Compatibility with other libraries

Representation of effects

About mtl

Future Plans

License

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

Your contributions are welcome!

Please see CONTRIBUTING.md.

Acknowledgements, citations, and related work

The following is a non-exhaustive list of people and works that have had a significant impact, directly or indirectly, on Heftia’s design and implementation: