This PR implements the open union by indexing the type from the tail end of the list. My thinking was that this way decomp and weaken does not need to do any index modification or allocation and can simply unsafeCoerce.
Basically I liked the idea of a "stable index".
The unfortunate consequence is that decomp along with any function using it gets an additional HasLen constraint. I implemented it at first using type level literals and a type level computation Len for type level lists, but this would have meant carrying a KnownNat (Len effs) constraint and furthermore it does not play nicely with partial lists, as the constraint does not carry through the type level computation, resulting in errors like could not deduce KnownNat (1 + Len effs) from a constraint KnwonNat (Len effs) etc.
Anyhow, this implementation works and passes the test suite. It does however run roughly twice as long 😞. It seems reallocating the union and decementing a Word value is cheaper than an additional, inlineable, compile time constant dict ...
As a result of the performance implications and the interface change I fully expect this PR to be rejected, but I figured I'd open it anyways, since I'd already done the work. Perhaps it'd make sense to park this in a branch somewhere, maybe Iit'll be of use some time in the future, who knows.
This PR implements the open union by indexing the type from the tail end of the list. My thinking was that this way
decompandweakendoes not need to do any index modification or allocation and can simplyunsafeCoerce.Basically I liked the idea of a "stable index".
The unfortunate consequence is that
decompalong with any function using it gets an additionalHasLenconstraint. I implemented it at first using type level literals and a type level computationLenfor type level lists, but this would have meant carrying aKnownNat (Len effs)constraint and furthermore it does not play nicely with partial lists, as the constraint does not carry through the type level computation, resulting in errors likecould not deduce KnownNat (1 + Len effs) from a constraint KnwonNat (Len effs)etc.Anyhow, this implementation works and passes the test suite. It does however run roughly twice as long 😞. It seems reallocating the union and decementing a
Wordvalue is cheaper than an additional, inlineable, compile time constant dict ...As a result of the performance implications and the interface change I fully expect this PR to be rejected, but I figured I'd open it anyways, since I'd already done the work. Perhaps it'd make sense to park this in a branch somewhere, maybe Iit'll be of use some time in the future, who knows.