Data.Union

Definitions

data Handler : List (Type -> Type) -> (Type -> Type) -> Type

  A list of effect handlers handling effects of types `fs`
  wrapping results in type `m`.

Totality: total
Visibility: public export
Constructors:

Nil : Handler [] m

(::) : (f x -> m x) -> Handler fs m -> Handler (f :: fs) m

data Union : List (Type -> Type) -> Type -> Type

  Sum type holding a value of type `t` wrapped in one of the
  effect types listed in `fs`.

Totality: total
Visibility: public export
Constructor: 

U : Has f fs -> f t -> Union fs t

Hints:

Has IO fs => HasIO (Free (Union fs))

Uninhabited (Union [] t)

inj : Has f fs => f t -> Union fs t

  Inject an effectful computation into a `Union`.

Totality: total
Visibility: public export

prj : Has f fs => Union fs t -> Maybe (f t)

  Tries to extract an effect from a `Union`.

Totality: total
Visibility: public export

prj1 : Union [f] t -> f t

  Extracts the last effect from a unary sum.

Totality: total
Visibility: public export

handleAll : Handler fs m -> Union fs t -> m t

  Handles all remaining effects via the given
  (heterogeneous) list of event handlers.

Totality: total
Visibility: public export

weaken1 : Union fs a -> Union (f :: fs) a

  Prepend a new effect to an existing `Union` value.

Totality: total
Visibility: public export

weaken : Subset fs fs' => Union fs a -> Union fs' a

Totality: total
Visibility: public export

decomp : {auto prf : Has f fs} -> Union fs a -> Either (Union (fs - f) a) (f a)

  Handle on of the effects in a `Union`. Unlike in other
  effect libraries, it's not necessary that the effect
  is the first in the list. To improve type inference,
  the return type is calculated from the `prf` value.

Totality: total
Visibility: public export

handle : {auto prf : Has f fs} -> (f a -> res) -> Union fs a -> Either (Union (fs - f) a) res

  Handle one of the effects in a `Union`. Unlike in other
  effect libraries, it's not necessary that the effect
  is the first in the list. To improve type inference,
  the return type is calculated from the `prf` value.

Totality: total
Visibility: public export