Added properties about DiffList in Data.DifferenceList.Properties

[mikedelorimier]

This adds Data.DifferenceList.Properties and moves Data.DifferenceList to Data.DifferenceList.Base. DiffList is like List but has efficient ++.

The new file is centered the new relation xs ~ ys between xs : List A and its equivalent ys : DiffList A. ~ is kind of like a simulation relation between List and DiffList. Each property shows preservation of a List op and its equivalent DiffList op. For example map⁺ relates List.map and DifferenceList.map:

map⁺ : (f : A → B) → xs ∼ ys → List.map f xs ∼ map f ys

It was easier for me to define and use properties on the relation xs ~ ys than properties on a transport function between List and DiffList (i.e. toList or fromList). The transport approach seemed complicated because there are many DiffLists that aren't equivalent to Lists.

This change is motivated by the characterization of Data.Tree.AVL.Indexed.toList, which was implemented using DiffList for efficiency. A followup PR for the AVL's toList will use this PR's []⁺ and ++-∷⁺ (pre-PR code is here). Properties also adds similar properties that seemed natural but are not currently used: ∼-fromList toList∘fromList toList⁺ fromList⁺ [_]⁺ ∷ʳ⁺ map⁺. So let me know if you'd like to review this one as a self-contained change or wait for followup PRs and review them all at once.

[mikedelorimier]

Why isn't there a take⁺ or drop⁺? Because take and drop don't preserve ~. For DiffList the take absorbs the ++:

(DiffList.take n ys) DiffList.++ ys′ ≡ DiffList.take n (ys DiffList.++ ys′)

Obvious the same isn't true for Lists: (List.take n xs) List.++ xs′ does not absorb the ++.

drop also passes a non-prepending function to lift, which means that it is not equivalent to List.drop. DiffList's take and list aren't used anywhere in the stdlib, so perhaps they should be renamed or removed.

[gallais]

Looks good; my only comments are on the old code :D

[jamesmckinna]

Thanks very much for this @mikedelorimier .

I wholeheartedly agree with the overhaul of this ancient piece of legacy code.

Where I disagree is on the implementation details, but I think the suggestions I offer are intended to expose more of the 'real' structure of what is going on... but YMMV.

I haven't commented on the Properties of functions sections, until such time as the dust settles on this first round of reviewing...

[jamesmckinna]

Oh, and as a suggested coda to all of the above:

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 3.0
lift : DiffList A → DiffList A → DiffList A
lift = _++_
{-# WARNING_ON_USAGE lift
"Warning: lift was deprecated in v3.0.
Please use _++_ instead."
#-}

[jamesmckinna]

You'll also need to add an entry to CHANGELOG to record this addition under New modules, such as

* `Data.DifferenceList` has been refactored to reexport the contents of two new modules:
  - `Data.DifferenceList.Base`
  - `Data.DifferenceList.Properties`

[jamesmckinna]

Subject to fixing the CHANGELOG, I think this is all good as it is, but maybe could be made a tiny bit more slick when it comes to delegating proofs of xs ∼ ys steps to the corresponding ones in terms of _≗_?

[gallais]

Why isn't there a take⁺ or drop⁺? Because take and drop don't preserve ~.

I think we should consider dropping these functions that are not law-abiding.

We may also want to name the pattern fromList ∘′ f ∘′ toList used in map
(maybe named viaList?) and prove a general result (is it provable?) of the form
xs ~ ys -> viaList f xs ~ f ys.

(Feel free to tell me to do it in a separate PR if you don't want to ;))

[mikedelorimier]

I think we should consider dropping these functions that are not law-abiding.

Makes sense, but can this and viaList be a followup PR? I'm unclear on how to format deprecated names that are planned for removal.

I updated the CHANGELOG's New modules, and I don't see any other pending comments.

[jamesmckinna]

@gallais if you added a second approval, I'd be happy to merge.