Control.Monad.MCancel

Reexports

Definitions

data Outcome : List Type -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Succeeded : a -> Outcome es a

Error : HSum es -> Outcome es a

Canceled : Outcome es a

Hints:

Applicative (Outcome es)

All Eq es => Eq a => Eq (Outcome es a)

Foldable (Outcome es)

Functor (Outcome es)

Monad (Outcome es)

All Show es => Show a => Show (Outcome es a)

Traversable (Outcome es)

toOutcome : Result es a -> Outcome es a

Totality: total
Visibility: export

fromOutcome : Outcome es a -> Result es (Maybe a)

Totality: total
Visibility: export

0 Poll : (List Type -> Type -> Type) -> Type

Totality: total
Visibility: public export

interface MCancel : (List Type -> Type -> Type) -> Type

Parameters: f
Constraints: MErr f
Methods:

canceled : f es ()

  Requests self-cancelation of the current fiber (computational thread).

uncancelable : (Poll f -> f es a) -> f es a

  Masks cancelation on the current fiber. The argument to `body` of type `Poll f` is a
  natural transformation `f ~> f` that enables polling. Polling causes a fiber to unmask
  within a masked region so that cancelation can be observed again.
  
  In the following example, cancelation can be observed only within `fb` and nowhere else:
  
  ```
    uncancelable $ \poll => fa >> poll(fb) >> fc
  ```
  
  If a fiber is canceled while it is masked, the cancelation is suppressed for as long as the
  fiber remains masked. Whenever the fiber is completely unmasked again, the cancelation will
  be respected.
  
  Masks can also be stacked or nested within each other. If multiple masks are active, all
  masks must be undone so that cancelation can be observed. In order to completely unmask
  within a multi-masked region the poll corresponding to each mask must be applied to the
  effect, outermost-first.
  
  ```
    uncancelable $ \p1 =>
      uncancelable $ \p2 =>
        fa >> p2(p1(fb)) >> fc
  ```
  
  The following operations are no-ops:
  
    1. Polling in the wrong order
    2. Subsequent polls when applying the same poll more than once: `poll(poll(fa))` is
       equivalent to `poll(fa)`
    3. Applying a poll bound to one fiber within another fiber

onCancel : f es a -> f [] () -> f es a

  Registers a finalizer that is invoked if cancelation is observed during the evaluation of
  `fa`. If the evaluation of `fa` completes without encountering a cancelation, the finalizer
  is unregistered before proceeding.
  
  Note that if `fa` is uncancelable (e.g. created via `uncancelable`) then `fin` won't be
  fired.
  
  ```
    onCancel (uncancelable(_ => canceled)) fin <-> F.unit
  ```
  
  During finalization, all actively registered finalizers are run exactly once. The order by
  which finalizers are run is dictated by nesting: innermost finalizers are run before
  outermost finalizers. For example, in the following program, the finalizer `f1` is run
  before the finalizer `f2`:
  
  ```
    onCancel (onCancel canceled f1) f2
  ```
  
  In accordance with the type signatur, finalizers must not throw observable
  errors

canceled : MCancel f => f es ()

  Requests self-cancelation of the current fiber (computational thread).

Totality: total
Visibility: public export

uncancelable : MCancel f => (Poll f -> f es a) -> f es a

  Masks cancelation on the current fiber. The argument to `body` of type `Poll f` is a
  natural transformation `f ~> f` that enables polling. Polling causes a fiber to unmask
  within a masked region so that cancelation can be observed again.
  
  In the following example, cancelation can be observed only within `fb` and nowhere else:
  
  ```
    uncancelable $ \poll => fa >> poll(fb) >> fc
  ```
  
  If a fiber is canceled while it is masked, the cancelation is suppressed for as long as the
  fiber remains masked. Whenever the fiber is completely unmasked again, the cancelation will
  be respected.
  
  Masks can also be stacked or nested within each other. If multiple masks are active, all
  masks must be undone so that cancelation can be observed. In order to completely unmask
  within a multi-masked region the poll corresponding to each mask must be applied to the
  effect, outermost-first.
  
  ```
    uncancelable $ \p1 =>
      uncancelable $ \p2 =>
        fa >> p2(p1(fb)) >> fc
  ```
  
  The following operations are no-ops:
  
    1. Polling in the wrong order
    2. Subsequent polls when applying the same poll more than once: `poll(poll(fa))` is
       equivalent to `poll(fa)`
    3. Applying a poll bound to one fiber within another fiber

Totality: total
Visibility: public export

onCancel : MCancel f => f es a -> f [] () -> f es a

  Registers a finalizer that is invoked if cancelation is observed during the evaluation of
  `fa`. If the evaluation of `fa` completes without encountering a cancelation, the finalizer
  is unregistered before proceeding.
  
  Note that if `fa` is uncancelable (e.g. created via `uncancelable`) then `fin` won't be
  fired.
  
  ```
    onCancel (uncancelable(_ => canceled)) fin <-> F.unit
  ```
  
  During finalization, all actively registered finalizers are run exactly once. The order by
  which finalizers are run is dictated by nesting: innermost finalizers are run before
  outermost finalizers. For example, in the following program, the finalizer `f1` is run
  before the finalizer `f2`:
  
  ```
    onCancel (onCancel canceled f1) f2
  ```
  
  In accordance with the type signatur, finalizers must not throw observable
  errors

Totality: total
Visibility: public export

guaranteeCase : MCancel f => f es a -> (Outcome es a -> f [] ()) -> f es a

  Specifies an effect that is always invoked after evaluation of `fa` completes, but depends
  on the outcome.
  
  See also `bracketCase` for a more powerful variant

Totality: total
Visibility: export

guarantee : MCancel f => f es a -> f [] () -> f es a

  Specifies an effect that is always invoked after evaluation of `fa` completes, regardless
  of the outcome.
  
  See `guaranteeCase` for a more powerful variant

Totality: total
Visibility: export

onAbort : MCancel f => f es a -> f [] () -> f es a

  Guarantees to run the given cleanup hook in case a fiber
  has been canceled or failed with an error.
  
  See `guaranteeCase` for additional information.

Totality: total
Visibility: export

bracketFull : MCancel f => (Poll f -> f es a) -> (a -> f es b) -> (a -> Outcome es b -> f [] ()) -> f es b

  A pattern for safely interacting with effectful lifecycles.
  
  If `acquire` completes successfully, `use` is called. If `use` succeeds, fails, or is
  canceled, `release` is guaranteed to be called exactly once.
  
  If `use` succeeds the returned value `B` is returned. If `use` returns an exception, the
  exception is returned.
  
  `acquire` is uncancelable by default, but can be unmasked. `release` is uncancelable. `use`
  is cancelable by default, but can be masked.

Totality: total
Visibility: export

bracketCase : MCancel f => f es a -> (a -> f es b) -> (a -> Outcome es b -> f [] ()) -> f es b

  A pattern for safely interacting with effectful lifecycles.
  
  If `acquire` completes successfully, `use` is called. If `use` succeeds, fails, or is
  canceled, `release` is guaranteed to be called exactly once.
  
  `acquire` is uncancelable. `release` is uncancelable. `use` is cancelable by default, but
  can be masked.

Totality: total
Visibility: export

bracket : MCancel f => f es a -> (a -> f es b) -> (a -> f [] ()) -> f es b

  A pattern for safely interacting with effectful lifecycles.
  
  If `acquire` completes successfully, `use` is called. If `use` succeeds, fails, or is
  canceled, `release` is guaranteed to be called exactly once.
  
  `acquire` is uncancelable. `release` is uncancelable. `use` is cancelable by default, but
  can be masked.

Totality: total
Visibility: export