NonScopedResumption.hs

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

import Control.Monad (join)
import Control.Monad.Hefty (Ask, Eff, Effect, FOEs, interpretBy, makeEffectF, runPure, type (:>))
import Control.Monad.Hefty.Reader (ask, runAsk)

-- This program is intended to demonstrate the behavior of Non-Scoped Resumptions in algebraic effects.
-- It is based on section 2.12.1 of the paper "Generalized Evidence Passing for Effect Handlers"
--    (  https://dl.acm.org/doi/pdf/10.1145/3473576  ).

-- The `Evil` effect, which returns a delimited continuation at the point of invocation.
data Evil es ans :: Effect where
    Evil :: Evil es ans f ()
makeEffectF ''Evil

-- Corresponds to `h_evil` in the paper.
runEvil :: forall es ans. (FOEs es) => Eff (Evil es ans : es) ans -> Eff es (Eff es ans)
runEvil = interpretBy (pure . pure) \Evil k -> pure $ join $ k ()

-- Interpret a Reader with a fixed value of 1.
-- Corresponds to `h_read` in the paper.
runRead1 :: Eff (Ask Int : es) a -> Eff es a
runRead1 = runAsk 1

-- Interpret a Reader with a fixed value of 2.
-- Corresponds to `h_read_2` in the paper.
runRead2 :: Eff (Ask Int : es) a -> Eff es a
runRead2 = runAsk 2

-- A effectful program that uses both `Ask` and `Evil` effects to test non-scoped resumption.
program :: (Ask Int :> es, Evil es' r :> es) => Eff es Int
program = do
    ask
    evil
    ask

-- Corresponds to `f` in the paper.
f :: Eff (Ask Int : es) a -> Eff es a
f = runRead2

-- Run the `Ask` and `Evil` interpreters and test non-scoped resumption.
-- If the result is 2, the algebraic effects are working correctly.
n :: Int
n = runPure do
    x <- runRead1 (runEvil program)
    f x

-- >>> n
-- 2

main :: IO ()
main = print n