{-# LANGUAGE BangPatterns, 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 :: forall (f :: AEffect) (ss :: Effects) a. HandlerBody f ss a -> ScopedEff f ss a -> Eff ss a handle HandlerBody f ss a h = HandlerBody' f ss a -> ScopedEff f ss a -> Eff ss a forall (f :: AEffect) (ss :: Effects) a. HandlerBody' f ss a -> ScopedEff f ss a -> Eff ss a handle' (\f x f Continuation ss0 ss x a k -> f x -> (x -> Eff ss a) -> Eff ss a HandlerBody f ss a h f x f (Continuation ss0 ss x a -> x -> Eff ss a forall (t :: Effects) (s :: Effects) b a. Continuation t s b a -> b -> Eff s a continue Continuation ss0 ss x a k)) -- | Generalization of 'handle' with cancellable continuations. handle' :: HandlerBody' f ss a -> ScopedEff f ss a -> Eff ss a handle' :: forall (f :: AEffect) (ss :: Effects) a. HandlerBody' f ss a -> ScopedEff f ss a -> Eff ss a handle' HandlerBody' f ss a h ScopedEff f ss a act = (forall (s :: Effects). PromptTag ss a s -> Eff (s :& ss) a) -> Eff ss a forall a (ss :: Effects). (forall (s :: Effects). PromptTag ss a s -> Eff (s :& ss) a) -> Eff ss a reset (\PromptTag ss a s p -> Handler f s -> Eff (s :& ss) a ScopedEff f ss a act (PromptTag ss a s -> HandlerBody' f ss a -> Handler f s forall (ss :: Effects) a (s :: Effects) (f :: AEffect). PromptTag ss a s -> HandlerBody' f ss a -> Handler f s MkHandler PromptTag ss a s p f x -> Continuation ss0 ss x a -> Eff ss a HandlerBody' f ss a h)) -- | Call an operation of algebraic effect @f@ with a handler. call :: s :> ss => Handler f s -> f a -> Eff ss a call :: forall (s :: Effects) (ss :: Effects) (f :: AEffect) a. (s :> ss) => Handler f s -> f a -> Eff ss a call (MkHandler PromptTag ss a s p HandlerBody' f ss a h) f a op = PromptTag ss a s -> (Continuation ss ss a a -> Eff ss a) -> Eff ss a forall (s :: Effects) a b (ss :: Effects) (ss0 :: Effects). (s :> ss0) => PromptTag ss a s -> (Continuation ss0 ss b a -> Eff ss a) -> Eff ss0 b shift0 PromptTag ss a s p (\Continuation ss ss a a k -> f a -> Continuation ss ss a a -> Eff ss a HandlerBody' f ss a h f a op Continuation ss ss a a 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)) -- @