data-effects-0.3.0.1: A basic framework for effect systems based on effects represented by GADTs.
Copyright(c) 2024 Sayo Koyoneda
LicenseMPL-2.0 (see the file LICENSE)
Maintainer[email protected]
Safe HaskellNone
LanguageGHC2021

Data.Effect.NonDet

Description

Effects that realize non-deterministic computations.

Synopsis

Documentation

data Empty a where Source #

An effect that eliminates a branch by causing the current branch context of a non-deterministic computation to fail.

Constructors

Empty :: forall a. Empty a

Eliminates a branch by causing the current branch context of a non-deterministic computation to fail.

pattern LEmpty :: forall a f a1. () => forall. (a ~ a1, ()) => LiftFOE Empty f a Source #

empty :: forall a f. SendFOE Empty f => f a Source #

Eliminates a branch by causing the current branch context of a non-deterministic computation to fail.

empty' :: forall {k} (tag :: k) a f. SendFOE (Tag Empty tag) f => f a Source #

Eliminates a branch by causing the current branch context of a non-deterministic computation to fail.

empty'' :: forall {k} (key :: k) a f. SendFOEBy key Empty f => f a Source #

Eliminates a branch by causing the current branch context of a non-deterministic computation to fail.

data Choose a where Source #

An effect that splits the computation into two branches.

Constructors

Choose :: Choose Bool

Splits the computation into two branches. As a result of executing choose, the world branches into one where False is returned and one where True is returned.

pattern LChoose :: forall a f. () => (a ~ Bool, ()) => LiftFOE Choose f a Source #

choose :: SendFOE Choose f => f Bool Source #

Splits the computation into two branches. As a result of executing choose, the world branches into one where False is returned and one where True is returned.

choose' :: forall {k} (tag :: k) f. SendFOE (Tag Choose tag) f => f Bool Source #

Splits the computation into two branches. As a result of executing choose, the world branches into one where False is returned and one where True is returned.

choose'' :: forall {k} (key :: k) f. SendFOEBy key Choose f => f Bool Source #

Splits the computation into two branches. As a result of executing choose, the world branches into one where False is returned and one where True is returned.

data ChooseH (f :: Type -> Type) a where Source #

An effect that executes two branches as scopes. A higher-order version of the Choose effect.

Constructors

ChooseH :: forall (f :: Type -> Type) a. f a -> f a -> ChooseH f a

Executes the given two scopes as branches. Even if one fails due to the empty operation, the whole does not fail as long as the other does not fail.

Instances

Instances details
() => HFunctor ChooseH Source # 
Instance details

Defined in Data.Effect.NonDet

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> ChooseH f :-> ChooseH g #

chooseH :: forall a f. SendHOE ChooseH f => f a -> f a -> f a Source #

Executes the given two scopes as branches. Even if one fails due to the empty operation, the whole does not fail as long as the other does not fail.

chooseH' :: forall {k} (tag :: k) a f. SendHOE (TagH ChooseH tag) f => f a -> f a -> f a Source #

Executes the given two scopes as branches. Even if one fails due to the empty operation, the whole does not fail as long as the other does not fail.

chooseH'' :: forall {k} (key :: k) a f. SendHOEBy key ChooseH f => f a -> f a -> f a Source #

Executes the given two scopes as branches. Even if one fails due to the empty operation, the whole does not fail as long as the other does not fail.