CatchFail.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 (when)
import Control.Monad.Hefty (Catch (Catch), Eff, Effect, Emb, FOEs, Throw, interpose, interpretBy, liftIO, makeEffectF, runEff, (:>))
import Control.Monad.Hefty.Except (catch, runExcept, throw)
import Data.List (singleton)
import Prelude hiding (fail)

{-

- This code is intended as an example that induces unsound semantics and will not compile in Heftia.

- If you use Haskell’s `eff` library, this code does compile, but -- as shown at the bottom -- the exception is not caught,
    which differs from the expected behavior.
    
- In Heftia, you can make it compile by *deliberately* opting into this “exceptions aren’t caught” behavior.

    - Specifically, you replace `runExcept (runChoice_... program)`
        with `runThrow @String (runChoice_... (runCatch program))`.
        
    - Why this counts as an intentional choice is explained in the "semantics of effects" section of
        the Heftia documentation:
        https://hackage-content.haskell.org/package/heftia-0.7.0.0/docs/Control-Monad-Hefty.html#semantics-of-effects


- `runChoice_...` provides two interpreters, allowing the user to freely choose which one to apply to `program`.

- `hookLoggingToCatch` exploits the higher-order effect nature of `catch`, i.e. the ability to
    dynamically modify (hook) its interpretation.

- What’s important here is `hookLoggingToCatch`. In the `program`, you can choose to hook `catchFail` or not,
    and the fact that the user can make that choice is a critical requirement for higher-order effects.

- By the way, it is indeed possible to write a program that directly implements the result of this “Expected behavior."
    Instead of throwing an exception in the runChoice function, you can use a function called hookThrowOnFail at a deeper
    level to rewrite the Fail behavior as a throw:
    https://gist.github.com/ymdryo/a2c6e97643c0e0d8bb9a4cacf08fb123
    However, in general cases, such a workaround won't always be available, and there will still be scenarios that
    can only be handled by having the interpreter itself throw at that point.
    In other words, what I'm aiming to demonstrate here is strictly the case of throwing within the runChoice interpreter.

-}

-- Non-deterministic computation effect
data Choice :: Effect where
    Fail :: String -> Choice m a -- Takes a string describing the reason for failure
    Choice :: Choice m Bool
makeEffectF ''Choice

-- Interpreter for Choice.
-- On failure, do not throw an exception, just discard that branch.
runChoice_NoThrowOnFail :: (FOEs es) => Eff (Choice : es) a -> Eff es [a]
runChoice_NoThrowOnFail = interpretBy (pure . singleton) \case
    Fail _reason -> \_k -> pure [] -- Discard the continuation `_k`
    Choice -> \k ->
        -- Branch the non-deterministic computation by calling the continuation `k` twice.
        -- Splits into the world where `choice` returns 'A' and the world where it returns 'B'.
        liftA2 (<>) (k False) (k True)

-- Interpreter for Choice, variant of runChoice_NoThrowOnFail.
-- On failure, throw an exception.
runChoice_ThrowOnFail :: (FOEs es, Throw String :> es) => Eff (Choice : es) a -> Eff es [a]
runChoice_ThrowOnFail = interpretBy (pure . singleton) \case
    Fail reason -> \_ -> throw reason -- Throw an exception
    Choice -> \k -> liftA2 (<>) (k False) (k True)

-- Hook logging into the `catch`
hookLoggingToCatch :: (Catch String :> es, Emb IO :> es) => Eff es a -> Eff es a
hookLoggingToCatch = interpose \(Catch action handleError) -> do
    catch
        do
            liftIO $ putStrLn "[LOG] Entering catch scope..."
            action
        \exception -> do
            liftIO $ putStrLn $ "[LOG] Caught exception: " <> exception
            handleError exception

-- Explore all combinations of Bool values for x and y,
-- and call `fail` when both x and y are True
failWhenBothTrue :: (Choice :> es, Emb IO :> es) => Eff es (Bool, Bool)
failWhenBothTrue = do
    x <- choice
    y <- choice

    when (x && y) (fail "x = y = True")
    liftIO $ putStrLn $ "x=" <> show x <> ", y=" <> show y
    pure (x, y)

-- Run `failWhenBothTrue` and catch any exception, printing the failure reason
catchFail :: (Choice :> es, Emb IO :> es, Catch String :> es) => Eff es (Maybe (Bool, Bool))
catchFail = do
    fmap Just failWhenBothTrue `catch` \reason -> do
        liftIO $ putStrLn $ "caught failure: " <> reason
        pure Nothing

-- Execute `catchFail`, hooking logging into its `catch`
program :: (Choice :> es, Emb IO :> es, Catch String :> es) => Eff es (Maybe (Bool, Bool))
program = hookLoggingToCatch catchFail

main :: IO ()
main = runEff do
    liftIO $ putStrLn "[NoThrowOnFail]"
    r1 <- runExcept @String (runChoice_NoThrowOnFail program)
    liftIO $ print r1

    liftIO $ putStrLn ""

    liftIO $ putStrLn "[ThrowOnFail]"
    r2 <- runExcept @String (runChoice_ThrowOnFail program)
    liftIO $ print r2

    pure ()

{-

Expected behavior:

[NoThrowOnFail]
[LOG] Entering catch scope...
x=False, y=False
x=False, y=True
x=True, y=False
Right [Just (False,False),Just (False,True),Just (True,False)]

[ThrowOnFail]
[LOG] Entering catch scope...
x=False, y=False
x=False, y=True
x=True, y=False
[LOG] Caught exception: x = y = True
caught failure: x = y = True
Right [Just (False,False),Just (False,True),Just (True,False),Nothing]

---

Incorrect behavior that would occur if no type error occurred:

[NoThrowOnFail]
[LOG] Entering catch scope...
x=False, y=False
x=False, y=True
x=True, y=False
Right [Just (False,False),Just (False,True),Just (True,False)]

[ThrowOnFail]
[LOG] Entering catch scope...
x=False, y=False
x=False, y=True
x=True, y=False
Left "x = y = True"

---

At present, there is no known effect system implementation capable of producing this expected behavior.
I'm curious because it might be possible to achieve with Kyo.
If that’s the case, it would be truly astonishing, and I think it’s amazing.

-}

Thank you for the explanation! It makes sense that it’s based on a multi-prompt monad. I believe there's a Haskell library called speff that used this approach to combine HOEs with algebraic effects. In fact, I once tried to integrate a multi-prompt monad myself, but it didn’t work out at the time. Encouraged by this Turbolift example, I'm going to try this approach again.

By the way, I've never seen the HOE approach using Control.delimit before. I suspect this is the key. It’s brilliant.

Good luck! Thanks for exploring nontrivial uses of algebraic effects and HOEs. I’m always eager to test if my design holds the water.