Nondeterministic Composite Destructuring

[loreanvictor]

Background

This is a proposed solution for resolving #8. Since the proposed solution requires further discussion and contemplation, I am creating a separate issue for it.

Proposed Solution

Allow for multi-part (composite) destructuring of arrays, in a non-deterministic manner:

{ ...a, ...b } : {1, 2, 3, 4, 5, 6};

In this example, one possible value for a and b would be {1, 2, 3} and {4, 5, 6} respectively. However, the destructuring is non-deterministic, as in there is no guarantee which split will be picked. The only given guarantee would be that:

IF there is a split would cause all destructuring elements to be non-empty, THEN the split picked (by the interpreter) would also assign non-empty lists to destructuring elements.

This means that for the composite destructuring specified above, all of these would be possible splits:

- a : {1}, b: {2, 3, 4, 5, 6}
- a: {1, 2, 3, 4, 5}, b: {6}
- a: {1, 2}, b: {3, 4, 5, 6}
...

but these wouldn't:

- a: {}, b: {1, 2, 3, 4, 5, 6}
- a: {1, 2, 3, 4, 5, 6}, b: {}

It is recommended for any implementation to prefer more balanced splits, i.e. those in which destructuring elements have roughly the same lengths, over other alternatives.

This proposal would also give meaning to following syntaxes:

{...rest, last}: some_list;
{first, ...rest, last}: some_list;
[{...left, center, ...right}]: some_expression;

and so on. The non rest elements of destructuring MUST be matched with elements of the destructured list. If that can't be done, an error should be thrown in case of static destructuring, and the rule MUST NOT be matched in case of parametric destructuring.

Benefits

The merge sort code in this gist is currently not syntactically-provable-total (it cannot be proven syntactically that it is total). With this change, the merge sort code might look like this:

{
  msort: {
    [{}]: {};
    [{...left, ...right}]: msort.merge[msort[left], msort[right]];

    merge[{a, ...ra}, {b, ...rb}]: {
      {a, ...msort.merge[ra, {b, ...rb}]}    | a < b;
      {b, ...msort.merge[{a, ...ra}, rb]}    | otherwise
    };
    merge[l, {}]: l;
    merge[{}, l]: l;
  }
}

Not only this presentation is more intuitive, it can also be syntactically proven that it is total (both msort and msort.merge). It is notable that the performance of the msort is dependent on whether the interpreter picks skewed splits or not. For example, if it prefers only one element for any destructuring element except the last, then the msort would become O(n^2), but if it picks balanced splits, then it would be O(n*log(n)).

Generally this increased flexibility allows for more intuitive representation for recursive computations, as evident in the merge sort example above. Another inspiring representation would be binary search:

{
  contains[x]: {
    [{}]: false;
    [{...left, center, ...right}]: {
      true                | x = center;
      left contains[x]    | x < center;
      right contains[x]   | x > center;
    }
  }
}

Problems

Object Destructuring Ambiguity

{ ...a, ...b }: { x: 2, y: 3, 4, 5 };

What is the value for a and b in this case? Assuming a balanced pick of split, a.length: 1, a[0]: 4 (similar for b), but it is unclear whether x should reside in a or b or both (similar for y).

Proposed work-around: distribution of constant keys is also non-deterministic and not guaranteed by the specification, but up to the implementation (without requirement for a guarantee of consistent behavior). The only requirement would be avoiding duplication of constant keys (so x cannot appear in both a and b).

Parametric Destructuring with Conditions

Z[{ ...a, x, ...b } | (x % 2) = 0]: {...a, ...b};

What should be the behavior in this case? There are two alternatives:

• The interpreter should search across matching splits and check if any of them satisfy given conditions. While this can be wildly useful, it can also be wildly computationally extensive and pretty complex. Besides, such checks are definitely not statically type-checkable any more (though we already have other matchings that are not statically type-checkable).

• The interpreter just picks a matching split, and will invoke the rule if the picked split also satisfies given condition. This is much more performant and pretty simple to implement, however this behavior would perhaps be pretty confusing for users of the language.

Note that since this is a pretty advanced use case, it might also be considered corner case and the decision between given alternatives even delegated to the implementation. However, we might discuss this further and reach the conclusion that this complex behavior is actually pretty desirable (or it generally should be consistent amongst implementations) and decide to enforce the choice in the spec.