Setting aside more radically distinct presentations such as explored in the experiments folder, we need to pick a path along the following trade-offs, some of which depend on one another.
Hardcoding some branches. Namely, there are essentially three candidates: Stuck, Guard, and Step. The alternative relies on predicating constructions that use them by a typeclass constraint of the shape B0 -< B for instance. Here the tradeoff is between bloating up case analyses on the structure of the tree, vs. carrying around almost universally needed class constraints.
Reflecting in the type signature the domain of delayed branches independently from the one of stepping branch. Compared to the current heterogeneous branch, this would add a fourth parameter to the datatype. On the obvious cons side, this bloats type signatures everywhere with parameters. On the positive side, this gives us a lot of flexibility to enforce static invariants: in particular, it allows us to easily specify the case where no delayed non-determinism is allowed, a situation somewhat reminiscent of guarded ccs, and notably used at the moment extensionally in the yield development.
Leveraging the result about so-called guarded encoding of stepping branches, establishing that stepping branches can always be encoded into guarded branches whose branches are guarded by Steps. This allow us to replace BrS from the datatype, assuming that we introduce explicitly Step. Naturally, it becomes incompatible with expressing statically that a computation is Guarded as suggested in 2.
Setting aside more radically distinct presentations such as explored in the
experimentsfolder, we need to pick a path along the following trade-offs, some of which depend on one another.Stuck,Guard, andStep. The alternative relies on predicating constructions that use them by a typeclass constraint of the shapeB0 -< Bfor instance. Here the tradeoff is between bloating up case analyses on the structure of the tree, vs. carrying around almost universally needed class constraints.yielddevelopment.guardedencoding of stepping branches, establishing that stepping branches can always be encoded into guarded branches whose branches are guarded bySteps. This allow us to replaceBrSfrom the datatype, assuming that we introduce explicitlyStep. Naturally, it becomes incompatible with expressing statically that a computation is Guarded as suggested in 2.