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.

-}

Hello @ymdryo !

Submitting my implementation in Scala 3 & Turbolift: https://gist.github.com/marcinzh/927fc54b8547ab21f2ce71020d734076

That's cool! As far as I know, this might be the first of its kind. I’m very curious about how the interaction between continuations and higher-order effects is implemented under the hood.

Honestly, I'd thought there were intrinsic limits to how flexibly one could combine algebraic effects with higher-order effects, so I’m really delighted to have found an example that overcomes them.

How was the type safety? When dealing with continuations, I imagine it often involves touching low-level parts of the runtime. Did you encounter any unexpected runtime errors during development? If it's a clean implementation that avoids those low-level details, then that's all the more impressive!

A bit of background:

1. My first effect system was Skutek, based on the Freer monad.

2. Due to inability to express HOEs, I started Turbolift, where I switched to a different technique: while keeping the monad-of-extensible-effects interface, I based the internals on monad transformers. This solved the HOE issue, but limited the range of expressible effects.

   Interestingly, Alexis King's initial eff design did something similar using Monad.Trans.Control.

3. I then encountered Scala Effekt (the old jfp branch), which introduced me to the "monad for multi-prompt delimited continuations". Through experimentation, I discovered it could be extended to support HOEs. I adopted this technique and rewrote Turbolift while retaining most of its original interface and typing.

The Turbolift implementation centers around two key components: 1) the main interpreter loop 2) the stack.

The main interpreter loop is centralized - it knows all effects in use at any given time and dispatches operations to their corresponding handlers. This differs from the Freer monad approach where each effect has its own interpreter loop that yields to the next one in the chain.

The stack uses a complex persistent data structure for performance reasons. For discussion purposes, we can model it as a simple immutable List[Frame] where some frames are Prompts. Each prompt is associated with a handler and a local state cell.

The local state is immutable - executing Local.put(s) creates a new stack copy.

Continuations are upper stack fragments obtained by splitting at a prompt (Control.capture).

HOEs are handled using Control.delimit (similar to reset), which pushes a clone of the current prompt onto the stack. This
makes this clone "shadow" the original from the interpreter's perspective. When exiting the scope, the original prompt and state become visible again.

I believe Alexis King's delimited continuations-based eff does something similar (minus the compiler patching for delimited continuation primitives). My Haskell knowledge (especially regarding advanced extensions) is too limited to say for certain.

Semantically, Turbolift behaves similarly to eff. See The effect semantics zoo and the corresponding ZooTest.scala

Regarding type safety & cleanliness:

The centralized interpreter loop operates on type-erased values (e.g., Any => Computation[Any, Any]). I guess this makes Turbolift somewhat unclean internally. Effekt implemented some evidence-carrying to address this.

Runtime errors primarily occurred during persistent stack optimizations. The stack implementation is highly complex, but this complexity is necessary for acceptable performance. The simpler List[Frame] model remains easier to reason about conceptually.

---

Appendix:

Here's a version of CatchFail that avoids using Control.shadow. The tradeoff is that we need to duplicate the original handler's implementation for all operations except catchAllEff.

https://gist.github.com/marcinzh/5e026d3410ae4fd21f1e0da4d5f1e3ab

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.