interaction trees
Abstractly, interaction trees are an appropriate adaptation of freer monads to settings that demand termination.
CoInductive itree (E : Type -> Type) (R : Type) : Type :=
| Ret (r : R)
| Tau (t : itree E R)
| Vis {A : Type} (e : E A) (k : E -> itree E R)
.