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
rDel
for 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 theSet
data type fromData.Set
:rDel set
will use aBool
fromset
, 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 becausenub
prefers elements later in a givenSet
than those earlier, andrDel
assumes the opposite. (For example,nub (Ext 3 (Ext 2 Empty))
keeps2
, but anrDel
implementation would keep3
.) Furthermore,nub
allows users to define custom merging behaviour whichrDel
does not support. This affects the definitions ofasSet
,asMap
andunion
.split
may 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 revertsplit
if 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!