Update to GHC 9.8.4 and use rearrangements to simplify value-level implementations #36
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The main change in this PR is the introduction of rearrangements, as detailed in Section 4 of Graded monads and type-level programming for dependence analysis (Keating and Gale, 2021) and in the README for the rearrangements library that spawned from that section. In short, this provides a generic value-level function
rDelfor arbitrary type-level sorts and filters by building the output type-indexed structure using elements of the input one. Consider the following example code, using theSetdata type fromData.Set:rDel setwill use aBoolfromset, then anInt, and finally a(), to construct its result to match its expected type. Notably, the type ofset'can be defined by a type family applied to the type ofset. This means that a function of type e.g.Set xs -> Set (Sorted xs)can be defined with justrDel.This matches many of the definitions in this library, so much of the complicated value-level redefinitions of type families have been rewritten to use
rDel. However, there are a few notes about this:nub, and definitions which rely on it, cannot userDel. This is becausenubprefers elements later in a givenSetthan those earlier, andrDelassumes the opposite. (For example,nub (Ext 3 (Ext 2 Empty))keeps2, but anrDelimplementation would keep3.) Furthermore,nuballows users to define custom merging behaviour whichrDeldoes not support. This affects the definitions ofasSet,asMapandunion.splitmay be less efficient now, but I cannot find evidence of this being the case: my concerns were because it now performs two passes through the inputSet(two calls torDel) rather than one more complex pass like the original definition. Since there is no obvious performance regression and the new code is cleaner, I think there's nothing to worry about. (Feel free to revertsplitif this is a concern!)quicksort!These changes are designed to preserve functionality without any breaking changes. All of the tests pass, and performance seems to be mostly unaffected from a quick comparison of test runtime.
This PR also updates the library to use GHC 9.8.4, which is the latest currently available in an LTS Stackage release (at time of writing, lts-23.10). Annoyingly, HLS doesn't yet support GHC 9.8.4, but hopefully it will in the near future!