Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Trade off in representations #23

Open
YaZko opened this issue Nov 26, 2022 · 0 comments
Open

Trade off in representations #23

YaZko opened this issue Nov 26, 2022 · 0 comments

Comments

@YaZko
Copy link
Contributor

YaZko commented Nov 26, 2022

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.

  1. 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.
  2. 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.
  3. 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant