Additional compositions with binary functions (#1259)

Author: Mathieu Montin

CHANGELOG.md

@@ -94,6 +94,10 @@ Deprecated names
   *-+-commutativeSemiring                ↦  +-*-commutativeSemiring
   *-+-isSemiringWithoutAnnihilatingZero  ↦  +-*-isSemiringWithoutAnnihilatingZero
   ```
+* In ̀Function.Basè:
+  ```
+  *_-[_]-_  ↦  _-⟪_⟫-_
+  ```
 
 * `Data.List.Relation.Unary.Any.any` to `Data.List.Relation.Unary.Any.any?`
 * `Data.List.Relation.Unary.All.all` to `Data.List.Relation.Unary.All.all?`
@@ -243,17 +247,17 @@ Other minor additions
 
 * Added new properties to `Data.Fin.Properties`:
   ```agda
-  toℕ≤n : (i : Fin n) → toℕ i ℕ.≤ n
-  ≤fromℕ : (i : Fin (ℕ.suc n)) → i ≤ fromℕ n
+  toℕ≤n             : (i : Fin n) → toℕ i ℕ.≤ n
+  ≤fromℕ            : (i : Fin (ℕ.suc n)) → i ≤ fromℕ n
   fromℕ<-irrelevant : m ≡ n → (m<o : m ℕ.< o) → (n<o : n ℕ.< o) → fromℕ< m<o ≡ fromℕ< n<o
-  fromℕ<-injective : fromℕ< m<o ≡ fromℕ< n<o → m ≡ n
-  inject₁ℕ< : (i : Fin n) → toℕ (inject₁ i) ℕ.< n
-  inject₁ℕ≤ : (i : Fin n) → toℕ (inject₁ i) ℕ.≤ n
-  ≤̄⇒inject₁< : i' ≤ i → inject₁ i' < suc i
-  ℕ<⇒inject₁< : toℕ i' ℕ.< toℕ i → inject₁ i' < i
-  toℕ-lower₁ : (p : m ≢ toℕ x) → toℕ (lower₁ x p) ≡ toℕ x
+  fromℕ<-injective  : fromℕ< m<o ≡ fromℕ< n<o → m ≡ n
+  inject₁ℕ<         : (i : Fin n) → toℕ (inject₁ i) ℕ.< n
+  inject₁ℕ≤         : (i : Fin n) → toℕ (inject₁ i) ℕ.≤ n
+  ≤̄⇒inject₁<       : i' ≤ i → inject₁ i' < suc i
+  ℕ<⇒inject₁<      : toℕ i' ℕ.< toℕ i → inject₁ i' < i
+  toℕ-lower₁        : (p : m ≢ toℕ x) → toℕ (lower₁ x p) ≡ toℕ x
   inject₁≡⇒lower₁≡ : (≢p : n ≢ (toℕ i')) → inject₁ i ≡ i' → lower₁ i' ≢p ≡ i
-  pred< : pred i < i
+  pred<              : pred i < i
   ```
 
 * Added new types and constructors to `Data.Integer.Base`:
@@ -356,10 +360,10 @@ Other minor additions
   cartesianProductWith⁻ : (∀ {x y} → R (f x y) → P x × Q y) → Any R (cartesianProductWith f xs ys) → Any P xs × Any Q ys
   cartesianProduct⁺     : Any P xs → Any Q ys → Any (P ⟨×⟩ Q) (cartesianProduct xs ys)
   cartesianProduct⁻     : Any (P ⟨×⟩ Q) (cartesianProduct xs ys) → Any P xs × Any Q ys
-  reverseAcc⁺ : ∀ acc xs → Any P acc ⊎ Any P xs → Any P (reverseAcc acc xs)
-  reverseAcc⁻ : ∀ acc xs → Any P (reverseAcc acc xs) -> Any P acc ⊎ Any P xs
-  reverse⁺ : Any P xs → Any P (reverse xs)
-  reverse⁻ : Any P (reverse xs) → Any P xs
+  reverseAcc⁺           : ∀ acc xs → Any P acc ⊎ Any P xs → Any P (reverseAcc acc xs)
+  reverseAcc⁻           : ∀ acc xs → Any P (reverseAcc acc xs) -> Any P acc ⊎ Any P xs
+  reverse⁺              : Any P xs → Any P (reverse xs)
+  reverse⁻              : Any P (reverse xs) → Any P xs
   ```
 
 * Added new proofs to `Data.List.Relation.Unary.Unique.Propositional.Properties`:
@@ -410,7 +414,7 @@ Other minor additions
 * Added new functions to `Data.String.Base`:
   ```agda
   wordsBy : Decidable P → String → List String
-  words : String → List String
+  words   : String → List String
   ```
 
 * Added new types and constructors to `Data.Nat.Base`:
@@ -485,9 +489,9 @@ Other minor additions
 
 * Added new functions to `Function.Base`:
   ```agda
-  _∘₂_ : (f : {x : A₁} → {y : A₂ x} → (z : B x y) → C z)
-       → (g : (x : A₁) → (y : A₂ x) → B x y)
-       → ((x : A₁) → (y : A₂ x) → C (g x y))
+  _∘₂_  : (f : {x : A₁} → {y : A₂ x} → (z : B x y) → C z)
+        → (g : (x : A₁) → (y : A₂ x) → B x y)
+        → ((x : A₁) → (y : A₂ x) → C (g x y))
 
   _∘₂′_ : (C → D) → (A → B → C) → (A → B → D)
   ```
@@ -499,55 +503,72 @@ Other minor additions
 
 * Added new functions to `Data.Fin.Base`:
   ```agda
-  quotRem : ∀ {n} k → Fin (n ℕ.* k) → Fin k × Fin n
+  quotRem  : ∀ {n} k → Fin (n ℕ.* k) → Fin k × Fin n
   opposite : ∀ {n} → Fin n → Fin n
   ```
 
 * Added new proofs to `Data.Fin.Properties`:
   ```agda
-  splitAt-< : ∀ m {n} i → (i<m : toℕ i ℕ.< m) → splitAt m {n} i ≡ inj₁ (fromℕ< i<m)
-  splitAt-≥ : ∀ m {n} i → (i≥m : toℕ i ℕ.≥ m) → splitAt m {n} i ≡ inj₂ (reduce≥ i i≥m)
+  splitAt-<         : ∀ m {n} i → (i<m : toℕ i ℕ.< m) → splitAt m {n} i ≡ inj₁ (fromℕ< i<m)
+  splitAt-≥         : ∀ m {n} i → (i≥m : toℕ i ℕ.≥ m) → splitAt m {n} i ≡ inj₂ (reduce≥ i i≥m)
   inject≤-injective : ∀ (n≤m n≤m′ : n ℕ.≤ m) x y → inject≤ x n≤m ≡ inject≤ y n≤m′ → x ≡ y
   ```
 
 * Added new proofs to `Data.Vec.Properties`:
   ```agda
-  unfold-take : ∀ n {m} x (xs : Vec A (n + m)) → take (suc n) (x ∷ xs) ≡ x ∷ take n xs
-  unfold-drop : ∀ n {m} x (xs : Vec A (n + m)) → drop (suc n) (x ∷ xs) ≡ drop n xs
+  unfold-take         : ∀ n {m} x (xs : Vec A (n + m)) → take (suc n) (x ∷ xs) ≡ x ∷ take n xs
+  unfold-drop         : ∀ n {m} x (xs : Vec A (n + m)) → drop (suc n) (x ∷ xs) ≡ drop n xs
   lookup-inject≤-take : ∀ m {n} (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) →
                         lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i
   ```
 
 * Added new functions to `Data.Vec.Functional`:
   ```agda
-  length : ∀ {n} → Vector A n → ℕ
-  insert : ∀ {n} → Vector A n → Fin (suc n) → A → Vector A (suc n)
-  updateAt : ∀ {n} → Fin n → (A → A) → Vector A n → Vector A n
-  _++_ : ∀ {m n} → Vector A m → Vector A n → Vector A (m ℕ.+ n)
-  concat : ∀ {m n} → Vector (Vector A m) n → Vector A (n ℕ.* m)
-  _>>=_ : ∀ {m n} → Vector A m → (A → Vector B n) → Vector B (m ℕ.* n)
+  length    : ∀ {n} → Vector A n → ℕ
+  insert    : ∀ {n} → Vector A n → Fin (suc n) → A → Vector A (suc n)
+  updateAt  : ∀ {n} → Fin n → (A → A) → Vector A n → Vector A n
+  _++_      : ∀ {m n} → Vector A m → Vector A n → Vector A (m ℕ.+ n)
+  concat    : ∀ {m n} → Vector (Vector A m) n → Vector A (n ℕ.* m)
+  _>>=_     : ∀ {m n} → Vector A m → (A → Vector B n) → Vector B (m ℕ.* n)
   unzipWith : ∀ {n} → (A → B × C) → Vector A n → Vector B n × Vector C n
-  unzip : ∀ {n} → Vector (A × B) n → Vector A n × Vector B n
-  take : ∀ m {n} → Vector A (m ℕ.+ n) → Vector A m
-  drop : ∀ m {n} → Vector A (m ℕ.+ n) → Vector A n
-  reverse : ∀ {n} → Vector A n → Vector A n
-  init : ∀ {n} → Vector A (suc n) → Vector A n
-  last : ∀ {n} → Vector A (suc n) → A
+  unzip     : ∀ {n} → Vector (A × B) n → Vector A n × Vector B n
+  take      : ∀ m {n} → Vector A (m ℕ.+ n) → Vector A m
+  drop      : ∀ m {n} → Vector A (m ℕ.+ n) → Vector A n
+  reverse   : ∀ {n} → Vector A n → Vector A n
+  init      : ∀ {n} → Vector A (suc n) → Vector A n
+  last      : ∀ {n} → Vector A (suc n) → A
   transpose : ∀ {m n} → Vector (Vector A n) m → Vector (Vector A m) n
   ```
 
+* Added a new simple function in `Function.Base`:
+  ```agda
+  constᵣ : A → B → B
+  ```
+
+* Added new compositions with a binary function in `Function.Base`:
+  ```agda
+  _-⟪_∣   : (A → B → C) → (C → B → D) → (A → B → D)
+  ∣_⟫-_   : (A → C → D) → (A → B → C) → (A → B → D)
+  _-⟨_∣   : (A → C) → (C → B → D) → (A → B → D)
+  ∣_⟩-_   : (A → C → D) → (B → C) → (A → B → D)
+  _-⟪_⟩-_ : (A → B → C) → (C → D → E) → (B → D) → (A → B → E)
+  _-⟨_⟫-_ : (A → C) → (C → D → E) → (A → B → D) → (A → B → E)
+  _-⟨_⟩-_ : (A → C) → (C → D → E) → (B → D) → (A → B → E)
+  _on₂_   : (C → C → D) → (A → B → C) → (A → B → D)
+  ```
+
 * Added new functions to `Data.Vec.Relation.Unary.All`:
   ```agda
   reduce : (f : ∀ {x} → P x → B) → All P xs → Vec B n
   ```
 
 * Added new proofs to `Data.Vec.Relation.Unary.All.Properties`:
   ```agda
-  All-swap : ∀ {xs ys} → All (λ x → All (x ~_) ys) xs → All (λ y → All (_~ y) xs) ys
+  All-swap  : ∀ {xs ys} → All (λ x → All (x ~_) ys) xs → All (λ y → All (_~ y) xs) ys
   tabulate⁺ : ∀ {f : Fin n → A} → (∀ i → P (f i)) → All P (tabulate f)
   tabulate⁻ : ∀ {f : Fin n → A} → All P (tabulate f) → (∀ i → P (f i))
-  drop⁺ : ∀ {n} m {xs} → All P {m + n} xs → All P {n} (drop m xs)
-  take⁺ : ∀ {n} m {xs} → All P {m + n} xs → All P {m} (take m xs)
+  drop⁺     : ∀ {n} m {xs} → All P {m + n} xs → All P {n} (drop m xs)
+  take⁺     : ∀ {n} m {xs} → All P {m + n} xs → All P {m} (take m xs)
   ```
 
 * Added new proofs to `Data.Vec.Membership.Propositional.Properties`:

src/Category/Applicative/Indexed.agda

@@ -53,7 +53,7 @@ record RawIApplicative {I : Set i} (F : IFun I f) :
   x <⊛ y = const <$> x ⊛ y
 
   _⊛>_ : ∀ {i j k} → F i j A → F j k B → F i k B
-  x ⊛> y = flip const <$> x ⊛ y
+  x ⊛> y = constᵣ <$> x ⊛ y
 
   _⊗_ : ∀ {i j k} → F i j A → F j k B → F i k (A × B)
   x ⊗ y = (_,_) <$> x ⊛ y

src/Category/Applicative/Predicate.agda

@@ -45,7 +45,7 @@ record RawPApplicative {I : Set i} (F : Pt I ℓ) :
   x <⊛ y = const <$> x ⊛ y
 
   _⊛>_ : ∀ {P Q} → const (∀ {i} → F P i) ⊆ F Q ⇒ F Q
-  x ⊛> y = flip const <$> x ⊛ y
+  x ⊛> y = constᵣ <$> x ⊛ y
 
   _⊗_ : ∀ {P Q} → F P ⊆ F Q ⇒ F (P ∩ Q)
   x ⊗ y = (_,_) <$> x ⊛ y

src/Data/Product.agda

@@ -153,7 +153,7 @@ swap : A × B → B × A
 swap (x , y) = (y , x)
 
 _-×-_ : (A → B → Set p) → (A → B → Set q) → (A → B → Set _)
-f -×- g = f -[ _×_ ]- g
+f -×- g = f -⟪ _×_ ⟫- g
 
 _-,-_ : (A → B → C) → (A → B → D) → (A → B → C × D)
-f -,- g = f -[ _,_ ]- g
+f -,- g = f -⟪ _,_ ⟫- g

src/Data/Sum/Base.agda

@@ -9,7 +9,7 @@
 module Data.Sum.Base where
 
 open import Data.Bool.Base using (true; false)
-open import Function.Base using (_∘_; _-[_]-_ ; id)
+open import Function.Base using (_∘_; _-⟪_⟫-_ ; id)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary using (Dec; yes; no; _because_; ¬_)
 open import Level using (Level; _⊔_)
@@ -64,7 +64,7 @@ map₂ = map id
 
 infixr 1 _-⊎-_
 _-⊎-_ : (A → B → Set c) → (A → B → Set d) → (A → B → Set (c ⊔ d))
-f -⊎- g = f -[ _⊎_ ]- g
+f -⊎- g = f -⟪ _⊎_ ⟫- g
 
 -- Conversion back and forth with Dec
 

src/Data/These.agda

@@ -40,7 +40,7 @@ leftMost : These A A → A
 leftMost = fold id id const
 
 rightMost : These A A → A
-rightMost = fold id id (flip const)
+rightMost = fold id id constᵣ
 
 mergeThese : (A → A → A) → These A A → A
 mergeThese = fold id id

src/Function/Base.agda

@@ -31,6 +31,9 @@ id x = x
 const : A → B → A
 const x = λ _ → x
 
+constᵣ : A → B → B
+constᵣ _ = id
+
 ------------------------------------------------------------------------
 -- Operations on dependent functions
 
@@ -164,8 +167,6 @@ case x of f = case x return _ of f
 ------------------------------------------------------------------------
 -- Operations that are only defined for non-dependent functions
 
-infixr 0 _-[_]-_
-infixl 1 _on_
 infixl 1 _⟨_⟩_
 infixl 0 _∋_
 
@@ -174,16 +175,6 @@ infixl 0 _∋_
 _⟨_⟩_ : A → (A → B → C) → B → C
 x ⟨ f ⟩ y = f x y
 
--- Composition of a binary function with a unary function
-
-_on_ : (B → B → C) → (A → B) → (A → A → C)
-_*_ on f = λ x y → f x * f y
-
--- Composition of three binary functions
-
-_-[_]-_ : (A → B → C) → (C → D → E) → (A → B → D) → (A → B → E)
-f -[ _*_ ]- g = λ x y → f x y * g x y
-
 -- In Agda you cannot annotate every subexpression with a type
 -- signature. This function can be used instead.
 
@@ -200,3 +191,67 @@ typeOf {A = A} _ = A
 
 it : {A : Set a} → {{A}} → A
 it {{x}} = x
+
+------------------------------------------------------------------------
+-- Composition of a binary function with other functions
+
+infixr 0 _-⟪_⟫-_ _-⟨_⟫-_
+infixl 0 _-⟪_⟩-_
+infixr 1 _-⟨_⟩-_ ∣_⟫-_ ∣_⟩-_
+infixl 1 _on_ _on₂_ _-⟪_∣ _-⟨_∣
+
+-- Two binary functions
+
+_-⟪_⟫-_ : (A → B → C) → (C → D → E) → (A → B → D) → (A → B → E)
+f -⟪ _*_ ⟫- g = λ x y → f x y * g x y
+
+-- A single binary function on the left
+
+_-⟪_∣ : (A → B → C) → (C → B → D) → (A → B → D)
+f -⟪ _*_ ∣ = f -⟪ _*_ ⟫- constᵣ
+
+-- A single binary function on the right
+
+∣_⟫-_ : (A → C → D) → (A → B → C) → (A → B → D)
+∣ _*_ ⟫- g = const -⟪ _*_ ⟫- g
+
+-- A single unary function on the left
+
+_-⟨_∣ : (A → C) → (C → B → D) → (A → B → D)
+f -⟨ _*_ ∣ = f ∘₂ const -⟪ _*_ ∣
+
+-- A single unary function on the right
+
+∣_⟩-_ : (A → C → D) → (B → C) → (A → B → D)
+∣ _*_ ⟩- g = ∣ _*_ ⟫- g ∘₂ constᵣ
+
+-- A binary function and a unary function
+
+_-⟪_⟩-_ : (A → B → C) → (C → D → E) → (B → D) → (A → B → E)
+f -⟪ _*_ ⟩- g = f -⟪ _*_ ⟫- ∣ constᵣ ⟩- g
+
+-- A unary function and a binary function
+
+_-⟨_⟫-_ : (A → C) → (C → D → E) → (A → B → D) → (A → B → E)
+f -⟨ _*_ ⟫- g = f -⟨ const ∣ -⟪ _*_ ⟫- g
+
+-- Two unary functions
+
+_-⟨_⟩-_ : (A → C) → (C → D → E) → (B → D) → (A → B → E)
+f -⟨ _*_ ⟩- g = f -⟨ const ∣ -⟪ _*_ ⟫- ∣ constᵣ ⟩- g
+
+-- A single binary function on both sides
+
+_on₂_ : (C → C → D) → (A → B → C) → (A → B → D)
+_*_ on₂ f = f -⟪ _*_ ⟫- f
+
+-- A single unary function on both sides
+
+_on_ : (B → B → C) → (A → B) → (A → A → C)
+_*_ on f = f -⟨ _*_ ⟩- f
+
+_-[_]-_ = _-⟪_⟫-_
+{-# WARNING_ON_USAGE _-[_]-_
+"Warning: Function._-[_]-_ was deprecated in v1.4.
+Please use _-⟪_⟫-_ instead."
+#-}

src/Function/Definitions.agda

@@ -19,13 +19,14 @@ module Function.Definitions
 open import Data.Product using (∃; _×_)
 import Function.Definitions.Core1 as Core₁
 import Function.Definitions.Core2 as Core₂
+open import Function.Base
 open import Level using (_⊔_)
 
 ------------------------------------------------------------------------
 -- Definitions
 
 Congruent : (A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
-Congruent f = ∀ {x y} → x ≈₁ y → f x ≈₂ f y
+Congruent f = ∀ {x y} → x ≈₁ y →  f x ≈₂ f y
 
 Injective : (A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
 Injective f = ∀ {x y} → f x ≈₂ f y → x ≈₁ y