Control.Effect.NonDet

Definitions

data ChoiceE : (Type -> Type) -> Type -> Type

  Add non-determinism to a computation,
  e.i. alternatives for program flow.
  Choice between these alternatives is not directly specified and is
  deferred to a particular handler.

Totality: total
Visibility: public export
Constructor: 

Choose : List (Inf (m a)) -> ChoiceE m a

Hint: 

Algebra sig m => Algebra (ChoiceE :+: sig) (ListT m)

Concat : Algebra sig m => Algebra (ChoiceE :+: sig) (ListT m)

  Handle choice by accumulating all alternatives in a list transformer.

Visibility: export

oneOf : Inj ChoiceE sig => Algebra sig m => List a -> m a

  Introduce non-deterministic branching to a computation.

Visibility: public export

oneOfM : Inj ChoiceE sig => Algebra sig m => List (Inf (m a)) -> m a

  Introduce non-deterministic branching to a computation.

Visibility: public export