Idris2Doc : Control.HigherOrder

Control.HigherOrder

(source)
Definitions
0 (~>) : (Type -> Type) -> (Type -> Type) -> Type
  Type of natural transformations between two functors.

  Visibility: public export
  Fixity Declaration: infixr operator, level 0
0 (~~>) : (Type -> Type) -> (Type -> Type) -> Type -> Type
  As above, but with explicit 0-morphisms.

  Visibility: public export
  Fixity Declaration: infixr operator, level 0
interface HFunctor : ((Type -> Type) -> Type -> Type) -> Type
  Higher-order functor, i.e. a functor
  in the category of functors and natural transformations.

  Parameters: h
Methods:
  
hmap : (Functor f, Functor g) => f ~> g -> h f ~> h g

Implementations:
  
HFunctor sig1 => HFunctor sig2 => HFunctor (sig1 :+: sig2)
  
Functor sig => HFunctor (Lift sig)
hmap : HFunctor h => (Functor f, Functor g) => f ~> g -> h f ~> h g
  Visibility: public export
data (:+:) : ((Type -> Type) -> Type -> Type) -> ((Type -> Type) -> Type -> Type) -> (Type -> Type) -> Type -> Type
  Higher-order disjoint union.
  Effects are composed via this datatype.

  Totality: total
  Visibility: public export
  Constructors:
  
Inl : sig1 m a -> (:+:) sig1 sig2 m a
  
Inr : sig2 m a -> (:+:) sig1 sig2 m a

  Hints:
  
HFunctor sig1 => HFunctor sig2 => HFunctor (sig1 :+: sig2)
  
Syntax sig1 => Syntax sig2 => Syntax (sig1 :+: sig2)

  Fixity Declaration: infixr operator, level 8
interface Prj : ((Type -> Type) -> Type -> Type) -> ((Type -> Type) -> Type -> Type) -> Type
  Higher order projections.
  Prj forms a category.

  Parameters: sup, sub
Constructor: 
MkPrj

Methods:
  
prj : sup m a -> sub m a
prj : Prj sup sub => sup m a -> sub m a
  Visibility: public export
interface Inj : ((Type -> Type) -> Type -> Type) -> ((Type -> Type) -> Type -> Type) -> Type
  Higher order injections.
  Inj forms a category.

  Parameters: sub, sup
Constructor: 
MkInj

Methods:
  
inj : sub m a -> sup m a

Implementation: 
Prj sub' sub => Inj sub sup => Inj sub' sup
inj : Inj sub sup => sub m a -> sup m a
  Visibility: public export
T : Inj siga sigb -> Inj sigb sigc -> Inj siga sigc
  Same as `Trans`, but the two arguments are explicit.

  Visibility: public export
0 Handler : (Type -> Type) -> (Type -> Type) -> (Type -> Type) -> Type
  State-preserving transformation of
  a computation in one monad into a computation
  in another monad, whose value is annotated with the final state.
  Handler is a natural transformation.

  Visibility: public export
0 HandlerX : (Type -> Type) -> (Type -> Type) -> (Type -> Type) -> Type -> Type
  Handler with explicit 0-morphism.

  Visibility: public export
interface Syntax : ((Type -> Type) -> Type -> Type) -> Type
  Parameters: sig
Constraints: HFunctor sig
Methods:
  
emap : (m a -> m b) -> sig m a -> sig m b
  Extend the continuation.
  
weave : Monad m => Monad n => Functor s => s () -> Handler s m n -> sig m a -> sig n (s a)
  Generically thread a handler through a higher-order
  signature.

Implementations:
  
Syntax sig1 => Syntax sig2 => Syntax (sig1 :+: sig2)
  
Functor sig => Syntax (Lift sig)
emap : Syntax sig => (m a -> m b) -> sig m a -> sig m b
  Extend the continuation.

  Visibility: public export
weave : Syntax sig => Monad m => Monad n => Functor s => s () -> Handler s m n -> sig m a -> sig n (s a)
  Generically thread a handler through a higher-order
  signature.

  Visibility: public export
data Lift : (Type -> Type) -> (Type -> Type) -> Type -> Type
  Lift a first-order functor to a second-order one.

  Totality: total
  Visibility: public export
  Constructor: 
MkLift : sig (m a) -> Lift sig m a

  Hints:
  
Functor sig => HFunctor (Lift sig)
  
Functor sig => Syntax (Lift sig)
unlift : Lift sig m a -> sig (m a)
  Visibility: public export
LiftE : (Type -> Type) -> (Type -> Type) -> Type -> Type
  Alias for use as an effect.

  Visibility: public export
(~<~) : Functor n => Functor ctx1 => HandlerX ctx1 m n q -> HandlerX ctx2 l m t -> HandlerX (ctx1 . ctx2) l n p
  Fuse two handlers.

  Visibility: public export
  Fixity Declaration: infixr operator, level 1