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.

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."
#-}

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`

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 ;))

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.

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