content: {-# LANGUAGE
    BangPatterns,
    DataKinds,
    GADTs,
    RankNTypes,
    ScopedTypeVariables,
    StandaloneKindSignatures,
    TypeOperators #-}
  
  -- | = Algebraic effects and named handlers
  --
  -- Algebraic effect handlers are a powerful framework for
  -- user-defined effects with a simple equational intuition.
  --
  -- Algebraic effect handlers are expressive enough to define various effects
  -- from scratch. In comparison, the 'Bluefin.State.runState' handler from
  -- "Bluefin.State" requires mutable references (@IORef@), relying on @IO@'s
  -- built-in statefulness. In terms of pure expressiveness, delimited
  -- continuations are all you need.
  --
  -- An "algebraic effect" is a signature for a set of operations which we
  -- represent with a GADT. For example, the "state effect" @State s@ contains
  -- two operations: @Get@ takes no parameter and returns a value of type @s@,
  -- and @Put@ takes a value of type @s@ and returns @()@. The constructors
  -- @Get@ and @Put@ are "uninterpreted operations": they only describe the types
  -- of arguments and results, with no intrinsic meaning.
  -- 
  -- @
  -- data 'Bluefin.Algae.State.State' s r where
  --   Get :: 'Bluefin.Algae.State.State' s s
  --   Put :: s -> 'Bluefin.Algae.State.State' s ()
  -- @
  --
  -- Below is an example of a stateful computation: a term of some type @'Eff' zz a@ with
  -- a state handler @h :: 'Handler' ('Bluefin.Algae.State.State' s) z@ in scope (@z :> zz@).
  -- The @State@ operations can be called using 'call' and the state handler @h@.
  --
  -- @
  -- -- Increment a counter and return its previous value.
  -- incr :: z :> zz => 'Handler' ('Bluefin.Algae.State.State' Int) z -> 'Eff' zz Int
  -- incr h = do
  --     n <- get
  --     put (n + 1)
  --     pure n
  --   where
  --     get = 'call' h Get
  --     put s = 'call' h (Put s)
  -- @
  --
  -- We handle the state effect by giving an interpretation of the @Get@ and @Put@
  -- operations, as a function @f :: 'HandlerBody' (State s) zz a@.
  --
  -- To 'call' @Get@ or @Put@ is to call the function @f@ supplied by 'handle'.
  -- The following equations show how 'handle' propagates an interpretation
  -- @f@ throughout a computation that calls @Get@ and @Put@:
  --
  -- @
  -- 'handle' f (\\h -> 'call' h Get     >>= k h) = f Get     ('handle' f (\\h -> k h))
  -- 'handle' f (\\h -> 'call' h (Put s) >>= k h) = f (Put s) ('handle' f (\\h -> k h))
  -- 'handle' f (\\h -> pure r) = pure r
  -- @
  --
  -- With those equations, @'handle' f@ applied to the above @incr@ simplifies to:
  --
  -- @
  -- 'handle' f incr =
  --   f Get \\n ->
  --   f (Put (n+1)) \\() ->
  --   pure n
  -- @
  --
  -- === References
  --
  -- - <https://homepages.inf.ed.ac.uk/gdp/publications/handling-algebraic-effects.pdf Handling Algebraic Effects> (2013) by Gordon D. Plotkin and Matija Pretnar.
  -- - <https://www.microsoft.com/en-us/research/uploads/prod/2021/05/namedh-tr.pdf First-class names for effect handlers> (2021) by Ningning Xie, Youyou Cong, and Daan Leijen.
  module Bluefin.Algae
    ( AEffect
  
      -- * Simple interface
    , HandlerBody
    , Handler
    , ScopedEff
    , handle
    , call
  
      -- * Cancellable continuations
      -- $cancel
    , HandlerBody'
    , handle'
    , continue
    , cancel
    ) where
  
  import Data.Kind (Type)
  import Bluefin.Eff (Eff, Effects, type (:&), type (:>))
  import Bluefin.Algae.DelCont
  
  -- | Algebraic effect.
  type AEffect = Type -> Type
  
  -- | Interpretation of an algebraic effect @f@: a function to handle the operations of @f@.
  type HandlerBody :: AEffect -> Effects -> Type -> Type
  type HandlerBody f ss a = (forall x. f x -> (x -> Eff ss a) -> Eff ss a)
  
  -- | Generalization of 'HandlerBody' with cancellable continuations.
  type HandlerBody' :: AEffect -> Effects -> Type -> Type
  type HandlerBody' f ss a = (forall ss0 x. f x -> Continuation ss0 ss x a -> Eff ss a)
  
  -- | Handler to call operations of the effect @f@.
  type Handler :: AEffect -> Effects -> Type
  data Handler f s where
    MkHandler :: !(PromptTag ss a s) -> HandlerBody' f ss a -> Handler f s
  
  -- | Effectful computation with in scope @ss@ and final result @a@,
  -- extended with a scoped algebraic effect @f@.
  --
  -- This type guarantees that the handler of @f@ cannot escape its scope:
  -- the 'Eff' computation cannot smuggle it out. All of the uses of the handle
  -- will happen in the span of the 'ScopedEff' computation.
  type ScopedEff f ss a = forall s. Handler f s -> Eff (s :& ss) a
  
  -- | Handle operations of @f@.
  --
  -- === Warning for exception-like effects
  --
  -- If the handler might not call the continuation (like for an exception effect), and
  -- if the handled computation manages resources (e.g., opening files, transactions)
  -- prefer 'handle'' to trigger resource clean up with cancellable continuations.
  handle ::
    HandlerBody f ss a ->
    ScopedEff f ss a ->
    Eff ss a
  handle h = handle' (\f k -> h f (continue k))
  
  -- | Generalization of 'handle' with cancellable continuations.
  handle' ::
    HandlerBody' f ss a ->
    ScopedEff f ss a ->
    Eff ss a
  handle' h act = reset (\p -> act (MkHandler p h))
  
  -- | Call an operation of algebraic effect @f@ with a handler.
  call :: s :> ss => Handler f s -> f a -> Eff ss a
  call (MkHandler p h) op = shift0 p (\k -> h op k)
  
  -- $cancel
  -- Cancellable continuations are useful to work with resource-management schemes
  -- with exception handlers such as 'Bluefin.Eff.bracket'
  --
  -- Cancellable continuations should be called exactly once (via 'continue' or 'cancel'):
  --
  -- - at least once to ensure resources are eventually freed (no leaks);
  -- - at most once to avoid use-after-free errors.
  --
  -- Enforcing this requirement with linear types would be a welcome contribution.
  --
  -- === Example
  --
  -- ==== Problem
  --
  -- Given 'Bluefin.Eff.bracket' and a @Fail@ effect,
  -- the simple 'Bluefin.Algae.handle' may cause resource leaks:
  --
  -- @
  -- 'Bluefin.Algae.handle' (\\_e _k -> pure Nothing)
  --   ('Bluefin.Eff.bracket' ex acquire release (\\_ -> 'call' h Fail))
  -- @
  --
  -- 'Bluefin.Eff.bracket' is intended to ensure that the acquired resource is
  -- released even if the bracketed function throws an exception. However, when
  -- the @Fail@ operation is called, the handler @(\\_e _k -> pure Nothing)@
  -- discards the continuation @_k@ which contains the exception handler
  -- installed by 'Bluefin.Eff.bracket'.
  -- The resource leaks because @release@ will never be called.
  --
  -- ==== Solution
  --
  -- Using 'handle'' instead lets us 'cancel' the continuation.
  --
  -- @
  -- 'handle'' (\\_e k -> 'cancel' k >> pure Nothing)
  --   ('Bluefin.Eff.bracket' acquire release (\\_ -> 'call' h Fail))
  -- @
  