a better scanr, via Data.List.NonEmpty

CHANGELOG.md

@@ -49,6 +49,15 @@ Deprecated names
   _-_  ↦  _//_
   ```
 
+* In `Data.List.Base`:
+  ```agda
+  scanr    ↦  Data.List.scanr
+  ```
+
+* In `Data.List.Properties`: (but not an exact replacement)
+  ```agda
+  scanr-defn   ↦  Data.List.NonEmpty.Properties.toList-scanr⁺
+
 * In `Data.Nat.Divisibility.Core`:
   ```agda
   *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
@@ -271,6 +280,26 @@ Additions to existing modules
   i*j≢0     : .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j)
   ```
 
+* In `Data.List`:
+  ```agda
+  scanr      : (A → B → B) → B → List A → List B
+  ```
+
+* In `Data.List.NonEmpty.Base`:
+  ```agda
+  tails⁺     : List A → List⁺ (List A)
+  scanr⁺     : (A → B → B) → B → List A → List⁺ B
+  ```
+
+* In `Data.List.NonEmpty.Properties`:
+  ```agda
+  toList-injective : toList xs ≡ toList ys → xs ≡ ys
+  toList-map    : (f : A → B) → toList ∘ map f ≗ List.map f ∘ toList
+  toList-tails⁺ : toList ∘ tails⁺ ≗ List.tails
+  scanr⁺-defn   : scanr⁺ f e ≗ map (List.foldr f e) ∘ tails⁺
+  toList-scanr⁺ : toList ∘ scanr⁺ f e ≗ List.map (List.foldr f e) ∘ List.tails
+  ```
+
 * In `Data.List.Properties`:
   ```agda
   applyUpTo-∷ʳ          : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n)

src/Data/List.agda

@@ -11,7 +11,30 @@
 
 module Data.List where
 
+import Data.List.NonEmpty.Base as List⁺
+open import Function.Base using (_∘_)
+
 ------------------------------------------------------------------------
 -- Types and basic operations
 
-open import Data.List.Base public
+open import Data.List.Base public hiding (scanr)
+
+------------------------------------------------------------------------
+-- scanr
+
+module _ {a b} {A : Set a} {B : Set b} (f : A → B → B) (e : B) where
+
+  open List⁺ using (toList; scanr⁺)
+
+-- definition
+
+  scanr : List A → List B
+  scanr = toList ∘ scanr⁺ f e
+
+{-
+-- which satisfies the following property:
+
+  scanr-defn : scanr ≗ map (foldr f e) ∘ tails
+  scanr-defn = Data.List.NonEmpty.Properties.toList-scanr⁺
+-}
+

src/Data/List/Base.agda

@@ -210,12 +210,6 @@ updateAt (x ∷ xs) (suc i) f = x ∷ updateAt xs i f
 
 -- Scans
 
-scanr : (A → B → B) → B → List A → List B
-scanr f e []       = e ∷ []
-scanr f e (x ∷ xs) with scanr f e xs
-... | []     = []                -- dead branch
-... | y ∷ ys = f x y ∷ y ∷ ys
-
 scanl : (A → B → A) → A → List B → List A
 scanl f e []       = e ∷ []
 scanl f e (x ∷ xs) = e ∷ scanl f (f e x) xs
@@ -570,3 +564,16 @@ _─_ = removeAt
 "Warning: _─_ was deprecated in v2.0.
 Please use removeAt instead."
 #-}
+
+-- Version 2.1
+
+scanr : (A → B → B) → B → List A → List B
+scanr f e []       = e ∷ []
+scanr f e (x ∷ xs) with scanr f e xs
+... | []         = []                -- dead branch
+... | ys@(y ∷ _) = f x y ∷ ys
+{-# WARNING_ON_USAGE scanr
+"Warning: scanr was deprecated in v2.1.
+Please use List.scanr instead."
+#-}
+

src/Data/List/NonEmpty/Base.agda

@@ -143,6 +143,21 @@ concatMap f = concat ∘′ map f
 ap : List⁺ (A → B) → List⁺ A → List⁺ B
 ap fs as = concatMap (λ f → map f as) fs
 
+-- Tails
+
+tails⁺ : List A → List⁺ (List A)
+tails⁺ xs = xs ∷ go xs
+  where
+  go : List A → List (List A)
+  go []       = []
+  go (x ∷ xs) = xs ∷ go xs
+
+-- Scanr
+
+scanr⁺ : (f : A → B → B) (e : B) → List A → List⁺ B
+scanr⁺ f e []       = e ∷ []
+scanr⁺ f e (x ∷ xs) = let y ∷ ys = scanr⁺ f e xs in f x y ∷ y ∷ ys
+
 -- Reverse
 
 reverse : List⁺ A → List⁺ A

src/Data/List/NonEmpty/Properties.agda

@@ -46,6 +46,9 @@ private
 η : ∀ (xs : List⁺ A) → head xs ∷ tail xs ≡ toList xs
 η _ = refl
 
+toList-injective : {xs ys : List⁺ A} → toList xs ≡ toList ys → xs ≡ ys
+toList-injective refl = refl
+
 toList-fromList : ∀ x (xs : List A) → x ∷ xs ≡ toList (x ∷ xs)
 toList-fromList _ _ = refl
 
@@ -113,6 +116,39 @@ map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (List.map-cong f≗g xs)
 map-∘ : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f
 map-∘ (x ∷ xs) = cong (_ ∷_) (List.map-∘ xs)
 
+toList-map : (f : A → B) → toList ∘ map f ≗ List.map f ∘ toList
+toList-map f (x ∷ xs) = refl
+
+------------------------------------------------------------------------
+-- tails
+
+toList-tails⁺ : toList ∘ tails⁺ ≗ List.tails {A = A}
+toList-tails⁺ []          = refl
+toList-tails⁺ ys@(_ ∷ xs) = cong (ys ∷_) (toList-tails⁺ xs)
+
+------------------------------------------------------------------------
+-- scanr
+
+module _ (f : A → B → B) (e : B) where
+
+  private
+    h = List.foldr f e
+
+  scanr⁺-defn : scanr⁺ f e ≗ map h ∘ tails⁺
+  scanr⁺-defn []       = refl
+  scanr⁺-defn (x ∷ xs) = let eq = scanr⁺-defn xs
+    in cong₂ (λ z → f x z ∷_) (cong head eq) (cong toList eq)
+
+  toList-scanr⁺ : toList ∘ scanr⁺ f e ≗ List.map h ∘ List.tails
+  toList-scanr⁺ xs = begin
+    toList (scanr⁺ f e xs)
+      ≡⟨ cong toList (scanr⁺-defn xs) ⟩
+    toList (map h (tails⁺ xs))
+      ≡⟨ toList-map h (tails⁺ xs) ⟩
+    List.map h (toList (tails⁺ xs))
+      ≡⟨ cong (List.map h) (toList-tails⁺ xs) ⟩
+    List.map h (List.tails xs) ∎
+
 ------------------------------------------------------------------------
 -- groupSeqs
 

src/Data/List/Properties.agda

@@ -8,6 +8,7 @@
 -- equalities than _≡_.
 
 {-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --warn=noUserWarning #-} -- for deprecated `scanr` (PR #2258)
 
 module Data.List.Properties where
 
@@ -618,18 +619,6 @@ sum-++ (x ∷ xs) ys = begin
 ∈⇒∣product {n} {n ∷ ns} (here  refl) = divides (product ns) (*-comm n (product ns))
 ∈⇒∣product {n} {m ∷ ns} (there n∈ns) = ∣n⇒∣m*n m (∈⇒∣product n∈ns)
 
-------------------------------------------------------------------------
--- scanr
-
-scanr-defn : ∀ (f : A → B → B) (e : B) →
-             scanr f e ≗ map (foldr f e) ∘ tails
-scanr-defn f e []             = refl
-scanr-defn f e (x ∷ [])       = refl
-scanr-defn f e (x ∷ y∷xs@(_ ∷ _))
-  with eq ← scanr-defn f e y∷xs
-  with z ∷ zs ← scanr f e y∷xs
-  = let z≡fy⦇f⦈xs , _ = ∷-injective eq in cong₂ (λ z → f x z ∷_) z≡fy⦇f⦈xs eq
-
 ------------------------------------------------------------------------
 -- scanl
 
@@ -1331,3 +1320,19 @@ map-─ = map-removeAt
 "Warning: map-─ was deprecated in v2.0.
 Please use map-removeAt instead."
 #-}
+
+-- Version 2.1
+
+scanr-defn : ∀ (f : A → B → B) (e : B) →
+             scanr f e ≗ map (foldr f e) ∘ tails
+scanr-defn f e []             = refl
+scanr-defn f e (x ∷ [])       = refl
+scanr-defn f e (x ∷ xs@(_ ∷ _))
+  with eq ← scanr-defn f e xs
+  with ys@(_ ∷ _) ← scanr f e xs
+  = cong₂ (λ z → f x z ∷_) (∷-injectiveˡ eq) eq
+{-# WARNING_ON_USAGE scanr-defn
+"Warning: scanr-defn was deprecated in v2.1.
+Please use Data.List.NonEmpty.toList-scanr⁺ instead."
+#-}
+