Heftia: higherorder effects done right for Haskell
Heftia is a higherorder effects version of Freer.
This library provides "continuationbased semantics" for higherorder effects, the same as lexilambda's eff.
Instead of using the IO
monad to implement delimited continuations for effects, Heftia internally uses Freer
monad.
The paper
 Casper Bach Poulsen and Cas van der Rest. 2023. Hefty Algebras: Modular
Elaboration of HigherOrder 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 higherorder 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.
We are looking forward to your feedback!
Getting Started
To run the SemanticsZoo example:
$ git clone https://github.com/sayohs/heftia
$ cd heftia/heftiaeffects
$ 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)])
[Note] All other permutations will cause type errors.
$
Example
Compared to existing Effect System libraries in Haskell that handle higherorder effects, this
library's approach allows for a more effortless and flexible handling of higherorder effects. Here
are some examples:
In handling higherorder effects, it's easy to work with multishot 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!"
(Preapplying behavior) ?
Or should it be "Hello world!!"
(Postapplying behavior) ?
With Heftia, you can freely choose either behavior depending on which higherorder 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 $ "Preapplying: " <> sPre
liftIO $ putStrLn $ "Postapplying: " <> sPost
Using the elabWriterPre
elaborator, you'll get "Goodbye world!", whereas with the elabWriterPost
elaborator, you'll get "Hello world!!".
Preapplying: Goodbye world!
Postapplying: 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 adhoc 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 heftiaeffects/Example/ directory.
Also, the following HeftWorld example: https://github.com/sayohs/HeftWorld
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.
Limitation and how to avoid it
The reset behavior of the scopes held by unhandled higherorder effects
When attempting to interpret an effect while there are unhandled higherorder effects present, you cannot obtain delimited continuations beyond the action scope held by these unhandled higherorder effects.
It appears as if a reset (in the sense of shift/reset) is applied to each of the scopes still held by the remaining unhandled higherorder effects.
In other words, to obtain delimited continuations beyond their scope, it is necessary to first handle and eliminate all higherorder effects that hold those scopes,
and then handle the effect targeted for stateful interpretation in that order.
For this purpose, it might sometimes be possible to use multilayering. For an example of multilayering,
see handleReaderThenShift
defined in Example/Continuation2
(particularly, the type signature of prog
within it).
For more details, please refer to the documentation of the interpretRec
family of functions.
Comparison
 HigherOrder Effects: Does it support higherorder effects?
 Delimited Continuation: The ability to manipulate delimited continuations.
 Statically Typed Set of Effects: For a term representing an effectful program, is it possible to statically decidable a type that enumerates all the effects the program may produce?
 Purely Monadic: Is an effectful program represented as a transparent data structure that is a monad, and can it be interpreted into other data types using only pure operations without side effects or
unsafePerformIO
?
 Dynamic Effect Rewriting: Can an effectful program have its internal effects altered afterwards (by functions typically referred to as
handle with
, intercept
, interpose
, transform
, translate
, or rewrite
) ?
 Performance: Time complexity or space complexity.
Library or Language 
HigherOrder Effects 
Delimited Continuation 
Statically Typed Set of Effects 
Purely Monadic 
Dynamic Effect Rewriting 
Performance (TODO) 
Heftia 
Yes 
Multishot 
Yes 
Yes (also Applicative and others) 
Yes 
? 
freersimple 
No 
Multishot 
Yes 
Yes 
Yes 
? 
Polysemy 
Yes 
No 
Yes 
Yes 
Yes 
? 
Effectful 
Yes 
No 
Yes 
No (based on the IO monad) 
Yes 
? 
eff 
Yes 
Multishot? 
Yes 
No (based on the IO monad) 
Yes 
Fast 
mtl 
Yes 
Multishot (ContT ) 
Yes 
Yes 
No 
? 
fusedeffects 
Yes 
No? 
Yes 
Yes 
No 
? 
kokalang 
No? 
Multishot 
Yes 
No (language builtin) 
? 
? 
OCamllang 5 
Yes 
Oneshot 
No 
No (language builtin) 
? 
? 
Heftia can simply be described as a higherorder version of freersimple.
This is indeed true in terms of its internal mechanisms as well.
Compatibility with other libraries
Representation of effects

Heftia Effects relies on dataeffects for the definitions of standard effects such as Reader
, Writer
, and State
.

It is generally recommended to use effects defined with automatic derivation provided by dataeffectsth.

The representation of firstorder effects is compatible with freersimple.
Therefore, effects defined for freersimple can be used as is in this library.
However, to avoid confusion between redundantly defined effects,
it is recommended to use the effects defined in dataeffects.

GADTs for higherorder effects need to be instances of the HFunctor type class for convenient usage.
While it is still possible to use them without being instances of HFunctor
,
the interpretRec
family of functions cannot be used when higherorder effects that are not HFunctor
are unhandled.
If this issue is not a concern, the GADT representation of higherorder effects is compatible with Polysemy and fusedeffects.
It is not compatible with Effectful and eff.
About mtl

Since the representation of effectful programs in Heftia is simply a monad (Eff
), it can be used as the base monad for transformers.
This means you can stack any transformer on top of it.

The Eff
monad is an instance of MonadIO
, MonadError
, MonadRWS
, etc., and these behave as the senders for the embedded IO
or the effect GADTs defined in dataeffects.
Future Plans
License
The license is MPL 2.0. Please refer to the NOTICE.
Additionally, this README.md and the documents under the docs
/docsja
directory are licensed
under CC BYSA 4.0.
Your contributions are welcome!
Please see CONTRIBUTING.md.
Credits
Parts of this project have been inspired by the following resources: