Thinking about the shuffle operator has been an interesting exercise in combining wrapper types with unary rules, to allow non-deterministic computation (creating multiple edges with different outputs). In fact, we could also view SLASH list insertion as a non-deterministic operation.
The way I presented wrapper types before, unifying the “input” data and the computation type triggers a type constraint, and this continues recursively, until we get a computation type that gives a defined result.
We can see a non-deterministic computation type as “missing” some information. If we know this information, we could continue the computation to get a result. So, we can have unary rules that supply different options for this missing information. For each way of completing the computation, we have a different unary rule, and a different output.
The unary rules can also recurse, to allow the number of “branching points” in the computation to depend on the input. For example, in the case of the shuffle operator, we need to have one sequence of unary rules for each permutation. We can decompose a permutation as a recursive series of decisions: we can see a permutation as first choosing which element to put at the start of the list, and then permuting the rest; we can see the choice of an element as maintaining a pointer into the list and choosing to either take the current element or increment the pointer.
Inserting an element somewhere in a list (or popping an element from somewhere in a list) is simpler than shuffling a list – for a list of length n, there are only n+1 options for pushing (and n options, for popping), rather than n! options for shuffling. In terms of the API, it would just look like:
SLASH.PUSH-ANYWHERE < #slash, [...] >
But this operation can only create the output list in the case where
#slash is empty. If
#slash is non-empty, this operation just sets up a data structure which needs to be the input for a unary rule. It will create a pointer to the beginning of the list, and then two unary rules could apply. One rule will say to insert the element at the current pointer position. The other rule will say to increment the pointer. Once all edges have recursively been added to the chart, there will be one edge for each possible SLASH list. (And also some extra edges for intermediate stages of computation. In this case, there would be n-1 extra edges. It would make sense to add a feature and a constraint to block these intermediate edges from participating in anything other than the non-deterministic computation rules.)
So using these non-deterministic
POP-ANYWHERE operations, we can simulate sets.