We currently restrict internal branching to finite branching, indexed by Fin types.
This is a clear restriction, and an immediate blocking point in experimental applications investigated by @nchappe.
Two possibilities:
Allow for indexation by either a Fin type, or by nat
Allow for indexation by an arbitrary type. In this case, the indexes used by a given computation must become a parameter of the datatype, similar to E for external interactions.
Exposing statically the indexes used in the second solution is mandatory if any notion akin to interpretation of internal non-determinism is to be defined in the future (and it shall!).
We currently restrict internal branching to finite branching, indexed by
Fin
types. This is a clear restriction, and an immediate blocking point in experimental applications investigated by @nchappe.Two possibilities:
Fin
type, or bynat
E
for external interactions.Exposing statically the indexes used in the second solution is mandatory if any notion akin to interpretation of internal non-determinism is to be defined in the future (and it shall!).