
   0 | module Control.Monad.MCancel
   1 | 
   2 | import public Control.Monad.MErr
   3 | 
   4 | %default total
   5 | 
   6 | --------------------------------------------------------------------------------
   7 | -- Outcome
   8 | --------------------------------------------------------------------------------
   9 | 
  10 | public export
  11 | data Outcome : List Type -> Type -> Type where
  12 |   Succeeded : (res : a) -> Outcome es a
  13 |   Error     : (err : HSum es) -> Outcome es a
  14 |   Canceled  : Outcome es a
  15 | 
  16 | export
  17 | All Eq es => Eq a => Eq (Outcome es a) where
  18 |   Succeeded x == Succeeded y = x == y
  19 |   Error x     == Error y     = x == y
  20 |   Canceled    == Canceled    = True
  21 |   _           == _           = False
  22 | 
  23 | export
  24 | All Show es => Show a => Show (Outcome es a) where
  25 |   showPrec p (Succeeded x) = showCon p "Succeeded" (showArg x)
  26 |   showPrec p (Error x)     = showCon p "Error" (showArg x)
  27 |   showPrec p Canceled      = "Canceled"
  28 | 
  29 | export
  30 | toOutcome : Result es a -> Outcome es a
  31 | toOutcome (Right v)   = Succeeded v
  32 | toOutcome (Left errs) = Error errs
  33 | 
  34 | export
  35 | fromOutcome : Outcome es a -> Result es (Maybe a)
  36 | fromOutcome (Succeeded v) = Right (Just v)
  37 | fromOutcome Canceled      = Right Nothing
  38 | fromOutcome (Error es)    = Left es
  39 | 
  40 | export
  41 | Functor (Outcome es) where
  42 |   map f (Succeeded v) = Succeeded (f v)
  43 |   map _ (Error v)     = Error v
  44 |   map _ Canceled      = Canceled
  45 | 
  46 | export
  47 | Foldable (Outcome es) where
  48 |   foldr f x (Succeeded v) = f v x
  49 |   foldr f x _             = x
  50 | 
  51 |   foldl f x (Succeeded v) = f x v
  52 |   foldl f x _             = x
  53 | 
  54 |   foldMap f (Succeeded v) = f v
  55 |   foldMap f _             = neutral
  56 | 
  57 |   toList (Succeeded v) = [v]
  58 |   toList _             = []
  59 | 
  60 |   null (Succeeded v) = False
  61 |   null _             = True
  62 | 
  63 | export
  64 | Traversable (Outcome es) where
  65 |   traverse f (Succeeded v) = Succeeded <$> f v
  66 |   traverse _ (Error v)     = pure $ Error v
  67 |   traverse _ Canceled      = pure Canceled
  68 | 
  69 | export
  70 | Applicative (Outcome es) where
  71 |   pure = Succeeded
  72 |   Succeeded f <*> Succeeded v = Succeeded (f v)
  73 |   Error err   <*> _           = Error err
  74 |   Canceled    <*> _           =  Canceled
  75 |   _           <*> Error err   = Error err
  76 |   _           <*> Canceled    = Canceled
  77 | 
  78 | export
  79 | Monad (Outcome es) where
  80 |   Succeeded v >>= f = f v
  81 |   Error x     >>= _ = Error x
  82 |   Canceled    >>= _ = Canceled
  83 | 
  84 | --------------------------------------------------------------------------------
  85 | -- MCancel
  86 | --------------------------------------------------------------------------------
  87 | 
  88 | public export
  89 | 0 Poll : (f : List Type -> Type -> Type) -> Type
  90 | Poll f = forall es,a . f es a -> f es a
  91 | 
  92 | public export
  93 | interface MErr f => MCancel f where
  94 |   ||| Requests self-cancelation of the current fiber (computational thread).
  95 |   canceled : f es ()
  96 | 
  97 |   ||| Masks cancelation on the current fiber. The argument to `body` of type `Poll f` is a
  98 |   ||| natural transformation `f ~> f` that enables polling. Polling causes a fiber to unmask
  99 |   ||| within a masked region so that cancelation can be observed again.
 100 |   |||
 101 |   ||| In the following example, cancelation can be observed only within `fb` and nowhere else:
 102 |   |||
 103 |   ||| ```
 104 |   |||   uncancelable $ \poll => fa >> poll(fb) >> fc
 105 |   ||| ```
 106 |   |||
 107 |   ||| If a fiber is canceled while it is masked, the cancelation is suppressed for as long as the
 108 |   ||| fiber remains masked. Whenever the fiber is completely unmasked again, the cancelation will
 109 |   ||| be respected.
 110 |   |||
 111 |   ||| Masks can also be stacked or nested within each other. If multiple masks are active, all
 112 |   ||| masks must be undone so that cancelation can be observed. In order to completely unmask
 113 |   ||| within a multi-masked region the poll corresponding to each mask must be applied to the
 114 |   ||| effect, outermost-first.
 115 |   |||
 116 |   ||| ```
 117 |   |||   uncancelable $ \p1 =>
 118 |   |||     uncancelable $ \p2 =>
 119 |   |||       fa >> p2(p1(fb)) >> fc
 120 |   ||| ```
 121 |   |||
 122 |   ||| The following operations are no-ops:
 123 |   |||
 124 |   |||   1. Polling in the wrong order
 125 |   |||   2. Subsequent polls when applying the same poll more than once: `poll(poll(fa))` is
 126 |   |||      equivalent to `poll(fa)`
 127 |   |||   3. Applying a poll bound to one fiber within another fiber
 128 |   uncancelable : (body: Poll f -> f es a) -> f es a
 129 | 
 130 |   ||| Registers a finalizer that is invoked if cancelation is observed during the evaluation of
 131 |   ||| `fa`. If the evaluation of `fa` completes without encountering a cancelation, the finalizer
 132 |   ||| is unregistered before proceeding.
 133 |   |||
 134 |   ||| Note that if `fa` is uncancelable (e.g. created via `uncancelable`) then `fin` won't be
 135 |   ||| fired.
 136 |   |||
 137 |   ||| ```
 138 |   |||   onCancel (uncancelable(_ => canceled)) fin <-> F.unit
 139 |   ||| ```
 140 |   |||
 141 |   ||| During finalization, all actively registered finalizers are run exactly once. The order by
 142 |   ||| which finalizers are run is dictated by nesting: innermost finalizers are run before
 143 |   ||| outermost finalizers. For example, in the following program, the finalizer `f1` is run
 144 |   ||| before the finalizer `f2`:
 145 |   |||
 146 |   ||| ```
 147 |   |||   onCancel (onCancel canceled f1) f2
 148 |   ||| ```
 149 |   |||
 150 |   ||| In accordance with the type signatur, finalizers must not throw observable
 151 |   ||| errors
 152 |   onCancel : f es a -> f [] () -> f es a
 153 | 
 154 | parameters {0    f  : List Type -> Type -> Type}
 155 |            {auto mc : MCancel f}
 156 | 
 157 |   ||| Specifies an effect that is always invoked after evaluation of `fa` completes, but depends
 158 |   ||| on the outcome.
 159 |   |||
 160 |   ||| See also `bracketCase` for a more powerful variant
 161 |   export
 162 |   guaranteeCase : f es a -> (Outcome es a -> f [] ()) -> f es a
 163 |   guaranteeCase act fin =
 164 |     uncancelable $ \poll => do
 165 |       v <- onError (onCancel (poll act) (fin Canceled)) (fin . Error)
 166 |       weakenErrors (fin $ Succeeded v)
 167 |       pure v
 168 | 
 169 |   ||| Specifies an effect that is always invoked after evaluation of `fa` completes, regardless
 170 |   ||| of the outcome.
 171 |   |||
 172 |   ||| See `guaranteeCase` for a more powerful variant
 173 |   export %inline
 174 |   guarantee : f es a -> f [] () -> f es a
 175 |   guarantee act = guaranteeCase act . const
 176 | 
 177 |   ||| Guarantees to run the given cleanup hook in case a fiber
 178 |   ||| has been canceled or failed with an error.
 179 |   |||
 180 |   ||| See `guaranteeCase` for additional information.
 181 |   export
 182 |   onAbort : f es a -> (cleanup : f [] ()) -> f es a
 183 |   onAbort as h =
 184 |     guaranteeCase as $ \case
 185 |       Canceled => h
 186 |       Error _  => h
 187 |       _        => pure ()
 188 | 
 189 |   ||| A pattern for safely interacting with effectful lifecycles.
 190 |   |||
 191 |   ||| If `acquire` completes successfully, `use` is called. If `use` succeeds, fails, or is
 192 |   ||| canceled, `release` is guaranteed to be called exactly once.
 193 |   |||
 194 |   ||| If `use` succeeds the returned value `B` is returned. If `use` returns an exception, the
 195 |   ||| exception is returned.
 196 |   |||
 197 |   ||| `acquire` is uncancelable by default, but can be unmasked. `release` is uncancelable. `use`
 198 |   ||| is cancelable by default, but can be masked.
 199 |   export
 200 |   bracketFull :
 201 |        (acquire : Poll f -> f es a)
 202 |     -> (use     : a -> f es b)
 203 |     -> (release : a -> Outcome es b -> f [] ())
 204 |     -> f es b
 205 |   bracketFull acquire use release =
 206 |     uncancelable $ \poll => do
 207 |       v <- acquire poll
 208 |       guaranteeCase (poll $ use v) (release v)
 209 | 
 210 |   ||| A pattern for safely interacting with effectful lifecycles.
 211 |   |||
 212 |   ||| If `acquire` completes successfully, `use` is called. If `use` succeeds, fails, or is
 213 |   ||| canceled, `release` is guaranteed to be called exactly once.
 214 |   |||
 215 |   ||| `acquire` is uncancelable. `release` is uncancelable. `use` is cancelable by default, but
 216 |   ||| can be masked.
 217 |   export %inline
 218 |   bracketCase :
 219 |        (acquire : f es a)
 220 |     -> (use     : a -> f es b)
 221 |     -> (release : a -> Outcome es b -> f [] ())
 222 |     -> f es b
 223 |   bracketCase = bracketFull . const
 224 | 
 225 |   ||| A pattern for safely interacting with effectful lifecycles.
 226 |   |||
 227 |   ||| If `acquire` completes successfully, `use` is called. If `use` succeeds, fails, or is
 228 |   ||| canceled, `release` is guaranteed to be called exactly once.
 229 |   |||
 230 |   ||| `acquire` is uncancelable. `release` is uncancelable. `use` is cancelable by default, but
 231 |   ||| can be masked.
 232 |   export %inline
 233 |   bracket :
 234 |        (acquire : f es a)
 235 |     -> (use     : a -> f es b)
 236 |     -> (release : a -> f [] ())
 237 |     -> f es b
 238 |   bracket acquire use release = bracketCase acquire use (const . release)
 239 |