Subset design

[axch]

From reviewing PR #963, a couple possible changes to the design of Subset.

1. Coercion

What if we change Subset a b to SafelyCoercible a b, i.e., where membership in this class guarantees both that a and b share a compatible representation and that a is a subset of b (at the representation level)?

Consequence: We'd probably want to represent RangeFrom q i (namely, (i..)) the same as q instead of with an offset, to retain the SafelyCoercible (RangeFrom q i) q instance.

Pro: Complicated subset relationships are guaranteed to be only type-level artifacts that do not perform runtime work.

Con?: The offset arithmetic moves to ordinal and unsafe_from_ordinal; how reliably can we get rid of it? That is, at the end of the day we probably want for k:(i..). to turn into

for (int k = i; k < n; k++)

instead of

for (int k' = 0; k' < n - i; k'++) {
  k = k' + i

But then again, maybe LLVM can just handle that.

2. Compatibility Law

Either Subset itself or another class should probably have a law guaranteeing compatibility with the ordering implied by Ix. The law in question would be

For i, j of type n, with constraints Ix n, Subset n m, Ix m, we have (ordinal i) < (ordinal j) implies (ordinal $ inject m i) < (ordinal $ inject m j).

This law is needed at least for the safety of the implementation of dual_inject in #963.

The coercion proposal is stronger than this, in that it implies similar compatibility laws for all other classes as well.

3. Many Injections

Without at least one of these interventions, the Subset class feels like it's badly misnamed, because what it actually defines is a set monomorphism (i.e., an injection) of which there are in general very many. The corresponding Lens construct is Prism, which is more like Dex isomorphisms than like class instances (exactly because any given types can have many different injections connecting them).

[axch]

By the way, Subset (with whatever name) should probably also expose a unsafe_project method.