Standard event types

State

Variant stateE (S : Type) : Type -> Type :=
| Get : stateE S S
| Put : S -> stateE S unit.

Reader

Variant readerE (R : Type) : Type -> Type :=
| Ask : readerE R R.

Writer

Variant writerE (W : Type) : Type -> Type :=
| Tell : W -> writerE W unit.

Exception

Variant exceptE (Err : Type) : Type -> Type :=
| Throw : Err -> exceptE Err void.

Nondeterminism

Variant nondetE : Type -> Type :=
| Or : nondetE bool.

Map

Variant mapE (K V : Type) : Type -> Type :=
| Insert : K -> V -> mapE unit
| Lookup : K -> mapE (option V)
| Remove : K -> mapE unit
.

Concurrency

Inductive spawnE (E : Type -> Type) : Type -> Type :=
| Spawn : itree (spawnE E +' E) unit -> spawnE E unit.

Dependent

 Variant depE {I : Type} (F : I -> Type) : Type -> Type :=
| Dep (i : I) : depE F (F i).