Control.Effect.Labelled

Definitions

data Labelled : k -> ((Type -> Type) -> Type -> Type) -> (Type -> Type) -> Type -> Type

  Wrap an effect in a label.
  This can help disambiguate between multiple identical effects and
  lessen the number of type annotations.

Totality: total
Visibility: public export
Constructor: 

MkLabelled : sub m a -> Labelled label sub m a

Hints:

Algebra (eff :+: sig) (sub m) => Algebra (Labelled label eff :+: sig) (Labelled label sub m)

Applicative (sub m) => Applicative (Labelled label sub m)

Functor (sub m) => Functor (Labelled label sub m)

Monad (sub m) => Monad (Labelled label sub m)

runLabelled : Labelled label sub m a -> sub m a

Visibility: public export

interface InjL : k -> ((Type -> Type) -> Type -> Type) -> ((Type -> Type) -> Type -> Type) -> Type

  Higher-order injections where signatures are inferred from the label.

Parameters: label, sub, sup
Constructor: 

MkSubL

Methods:

injLabelled : Labelled label sub m a -> sup m a

injLabelled : InjL label sub sup => Labelled label sub m a -> sup m a

Visibility: public export

Label : Inj sub sup -> InjL label sub sup

Visibility: public export

labelled : (label : k) -> InjL label sub sig => Algebra sig m => sub m a -> m a

Visibility: public export