[Added curry and uncurry.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101210173923
 Ignore-this: 3f9c5dba8c9be16ab950bd3d88acfc56
] hunk ./ReverseComposition.agda 14
-open import Data.Product using (∃; ,_; proj₁; proj₂)
-open import Data.Unit using (tt)
+open import Data.Product using (_×_; _,_; ∃; ,_; proj₁; proj₂)
+open import Data.Unit using (⊤; tt)
hunk ./ReverseComposition.agda 19
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_)
hunk ./ReverseComposition.agda 43
-------------------------------------------------------------------------
--- A specialised variant of _⇨_
-
-infixr 5 _↑_⇨_
-
-_↑_⇨_ : ∀ {ℓ} → Set ℓ → ℕ → Set ℓ → Set (suc ℓ)
-A ↑ n ⇨ B = List.replicate n A ⇨ B
-
--- Applies the function to a vector of arguments.
-
-app : ∀ {ℓ} {A B : Set ℓ} {n} → A ↑ n ⇨ B → Vec A n → B
-app {n = zero}  x []       = ! x
-app {n = suc n} f (x ∷ xs) = app (f · x) xs
-
hunk ./ReverseComposition.agda 248
+------------------------------------------------------------------------
+-- Generalised currying
+
+Args : ∀ {ℓ} → List (Set ℓ) → Set ℓ
+Args = List.foldr _×_ (Lift ⊤)
+
+uncurry : ∀ {ℓ As} {B : Set ℓ} → As ⇨ B → (Args As → B)
+uncurry (return x) _        = x
+uncurry (Λ f)      (a , as) = uncurry (f a) as
+
+curry : ∀ {ℓ As} {B : Set ℓ} → (Args As → B) → As ⇨ B
+curry {As = []}     f = return (f _)
+curry {As = A ∷ As} f = Λ λ a → curry (λ as → f (a , as))
+
+module CurryLaws {ℓ} where
+
+  curry∘uncurry : ∀ {As} {B : Set ℓ} (f : As ⇨ B) →
+                  curry {As = As} (uncurry f) ≈ f
+  curry∘uncurry (return x) = return P.refl
+  curry∘uncurry (Λ f)      = Λ λ a → curry∘uncurry (f a)
+
+  uncurry∘curry : ∀ As {B : Set ℓ} (f : Args As → B) →
+                  uncurry (curry {As = As} f) ≗ f
+  uncurry∘curry []       f as = P.refl
+  uncurry∘curry (A ∷ As) f as = uncurry∘curry As _ _
+
+  curry-cong : ∀ {As} {B : Set ℓ} {f₁ f₂ : Args As → B} →
+               f₁ ≗ f₂ → curry {As = As} f₁ ≈ curry {As = As} f₂
+  curry-cong {[]}     f₁≗f₂ = return (f₁≗f₂ _)
+  curry-cong {A ∷ As} f₁≗f₂ = Λ λ a → curry-cong (λ as → f₁≗f₂ (a , as))
+
+  uncurry-cong : ∀ {As} {B : Set ℓ} {f₁ f₂ : As ⇨ B} →
+                 f₁ ≈ f₂ → uncurry f₁ ≗ uncurry f₂
+  uncurry-cong (return x₁≡x₂) _        = x₁≡x₂
+  uncurry-cong (Λ f₁≈f₂)      (a , as) = uncurry-cong (f₁≈f₂ a) as
+
+------------------------------------------------------------------------
+-- A specialised variant of _⇨_
+
+infixr 5 _↑_⇨_
+
+_↑_⇨_ : ∀ {ℓ} → Set ℓ → ℕ → Set ℓ → Set (suc ℓ)
+A ↑ n ⇨ B = List.replicate n A ⇨ B
+
+-- Applies the function to a vector of arguments.
+--
+-- Note that app is morally a special case of uncurry.
+
+app : ∀ {ℓ} {A B : Set ℓ} {n} → A ↑ n ⇨ B → Vec A n → B
+app {n = zero}  x []       = ! x
+app {n = suc n} f (x ∷ xs) = app (f · x) xs
+
hunk ./ReverseComposition.agda 307
-return∥ {As = []}     x = return x
-return∥ {As = A ∷ As} x = Λ λ _ → return∥ x
+return∥ {As = As} x = curry {As = As} (const x)
hunk ./ReverseComposition.agda 487
+  -- _>>=∥_ can be defined using curry and uncurry.
+
+  >>=∥-curry-uncurry :
+    ∀ {As} {B C : Set ℓ} (f : As ⇨ B) (g : B → As ⇨ C) →
+    f >>=∥ g ≈ curry {As = As} (λ as → uncurry (g (uncurry f as)) as)
+  >>=∥-curry-uncurry (return x) g with g x
+  ... | return y =
+    return y                       ≡⟨ P.refl ⟩
+    return (uncurry (return y) _)  ∎
+  >>=∥-curry-uncurry (Λ {As = As} f) g = Λ λ a →
+    let h = λ (as : Args As) → g (uncurry (f a) as) in
+    (f a >>=∥ λ y → g y · a)                            ≈⟨ >>=∥-curry-uncurry (f a) (λ y → g y · a) ⟩
+    curry (λ as → uncurry (h as · a) as)                ≡⟨ P.refl ⟩
+    curry (λ as → uncurry (Λ λ x → h as · x) (a , as))  ≈⟨ curry-cong (λ as → uncurry-cong (complete (η {f = h as})) (a , as)) ⟩
+    curry (λ as → uncurry (h as) (a , as))              ∎
+    where open CurryLaws
+
+  -- _⊛∥_ can be defined using curry and uncurry.
+
+  ⊛∥-curry-uncurry :
+    ∀ {As} {B C : Set ℓ} (f : As ⇨ (B → C)) (g : As ⇨ B) →
+    f ⊛∥ g ≈ curry {As = As} (λ as → (uncurry f as) (uncurry g as))
+  ⊛∥-curry-uncurry {As} f g =
+    (f >>=∥ λ h → g >>=∥ λ x → return∥ (h x))                                 ≈⟨ >>=∥-curry-uncurry f _ ⟩
+    curry (λ as → uncurry (g >>=∥ λ x → return∥ (uncurry f as x)) as)         ≈⟨ curry-cong (λ as →
+                                                                                   uncurry-cong {As = As}
+                                                                                     (>>=∥-curry-uncurry g (return∥ ∘ uncurry f as))
+                                                                                     as) ⟩
+    curry (λ as →
+      uncurry (curry {As = As} (λ as′ →
+        uncurry (return∥ {As = As} (uncurry f as (uncurry g as′))) as′)) as)  ≈⟨ curry-cong (λ as →
+                                                                                   uncurry∘curry As
+                                                                                     (λ as′ → uncurry
+                                                                                                (return∥ {As = As}
+                                                                                                         (uncurry f as (uncurry g as′)))
+                                                                                                as′)
+                                                                                     as) ⟩
+    curry (λ as →
+        uncurry (return∥ {As = As} (uncurry f as (uncurry g as))) as)         ≈⟨ curry-cong (λ as →
+                                                                                   uncurry∘curry As (λ _ → uncurry f as (uncurry g as))
+                                                                                                 as) ⟩
+    curry (λ as → uncurry f as (uncurry g as))                                ∎
+    where open CurryLaws
+