{-# LANGUAGE FlexibleContexts, TypeOperators, DataKinds #-} {-# LANGUAGE Safe #-} -- | An example of non-trivial interaction of effects, handling of two -- effects together -- Non-determinism with control (cut) -- For the explanation of cut, see Section 5 of Hinze ICFP 2000 paper. -- Hinze suggests expressing cut in terms of cutfalse: -- -- > = return () `mplus` cutfalse -- > where -- > cutfalse :: m a -- -- satisfies the following laws: -- -- > cutfalse >>= k = cutfalse (F1) -- > cutfalse | m = cutfalse (F2) -- -- (note: @m \``mplus`\` cutfalse@ is different from @cutfalse \``mplus`\` m@). -- In other words, cutfalse is the left zero of both bind and mplus. -- -- Hinze also introduces the operation @`call` :: m a -> m a@ that -- delimits the effect of cut: @`call` m@ executes m. If the cut is -- invoked in m, it discards only the choices made since m was called. -- Hinze postulates the axioms of `call`: -- -- > call false = false (C1) -- > call (return a | m) = return a | call m (C2) -- > call (m | cutfalse) = call m (C3) -- > call (lift m >>= k) = lift m >>= (call . k) (C4) -- -- @`call` m@ behaves like @m@ except any cut inside @m@ has only a local effect, -- he says. -- -- Hinze noted a problem with the \"mechanical\" derivation of backtracing -- monad transformer with cut: no axiom specifying the interaction of -- call with bind; no way to simplify nested invocations of call. -- -- We use exceptions for cutfalse -- Therefore, the law @cutfalse >>= k = cutfalse@ -- is satisfied automatically since all exceptions have the above property. module Control.Eff.Cut where import Control.Eff import Control.Eff.Exception import Control.Eff.Choose data CutFalse = CutFalse cutfalse :: Member (Exc CutFalse) r => Eff r a cutfalse = throwError CutFalse -- | The interpreter -- it is like reify . reflect with a twist. Compare this -- implementation with the huge implementation of call in Hinze 2000 (Figure 9). -- Each clause corresponds to the axiom of call or cutfalse. All axioms are -- covered. -- -- The code clearly expresses the intuition that call watches the choice points -- of its argument computation. When it encounteres a cutfalse request, it -- discards the remaining choicepoints. It completely handles CutFalse effects -- but not non-determinism call :: forall a r. Member Choose r => Eff (Exc CutFalse ': r) a -> Eff r a call m = loop [] m where loop :: Member Choose r => [Eff (Exc CutFalse ': r) a] -> Eff (Exc CutFalse ': r) a -> Eff r a loop jq (Val x) = return x `mplus'` next jq -- (C2) loop jq (E u q) = case decomp u of Right (Exc CutFalse) -> mzero' -- drop jq (F2) Left u0 -> check jq u0 q check :: forall b. [Eff (Exc CutFalse ': r) a] -> Union r b -> Arrs (Exc CutFalse ': r) b a -> Eff r a check jq u _ | Just (Choose []) <- prj u = next jq -- (C1) check jq u q | Just (Choose [x]) <- prj u = loop jq (q ^$ x) -- (C3), optim check jq u q | Just (Choose lst) <- prj u = next $ map (q ^$) lst ++ jq -- (C3) check jq u q = loop jq (E (weaken u) q) -- (C4) next :: Member Choose r => [Eff (Exc CutFalse ': r) a] -> Eff r a next [] = mzero' next (h:t) = loop t h