Abstract currying in Agda

Curry.agda

module Curry where

module And where

  data And : Set → Set → Set where
    and : (X Y : Set) → X → Y → And X Y

  curry
    : (X Y Z : Set)
    → (And X Y → Z)
    → (X → Y → Z)
  curry X Y Z f x y = f (and X Y x y)

  uncurry
    : (X Y Z : Set)
    → (X → Y → Z)
    → (And X Y → Z)
  uncurry X Y Z f (and .X .Y x y) = f x y

module Abstract where

  curry
    : (F : Set → Set → Set)
    → (d : (P Q : Set) → P → Q → F P Q)
    → (X Y Z : Set)
    → (F X Y → Z)
    → (X → Y → Z)
  curry F d X Y Z f x y = f (d X Y x y)

  uncurry
    : (F : Set → Set → Set)
    → (p1 : (P Q : Set) → F P Q → P)
    → (p2 : (P Q : Set) → F P Q → Q)
    → (X Y Z : Set)
    → (X → Y → Z)
    → (F X Y → Z)
  uncurry F p1 p2 X Y Z f d = f (p1 X Y d) (p2 X Y d)


andCurry
  : (X Y Z : Set)
  → (And.And X Y → Z)
  → (X → Y → Z)
andCurry = Abstract.curry And.And And.and

andUncurry
  : (X Y Z : Set)
  → (X → Y → Z)
  → (And.And X Y → Z)
andUncurry = Abstract.uncurry And.And p1 p2 where
  p1 : (P Q : Set) → (And.And P Q) → P
  p1 P Q (And.and .P .Q p q) = p

  p2 : (P Q : Set) → (And.And P Q) → Q
  p2 P Q (And.and .P .Q p q) = q


module Annoying where
  open import Agda.Primitive

  curry
    : (F : {a b : Level} → Set a → Set b → Set (a ⊔ b))
    → (d : {a b : Level} → (P : Set a) (Q : Set b) → P → Q → F P Q)
    → {a b c : Level}
    → (X : Set a) (Y : Set b) (Z : Set c)
    → (F X Y → Z)
    → (X → Y → Z)
  curry F d X Y Z f x y = f (d X Y x y)

  uncurry
    : (F : {a b : Level} → Set a → Set b → Set (a ⊔ b))
    → (p1 : {a b : Level} → (P : Set a) (Q : Set b) → F P Q → P)
    → (p2 : {a b : Level} → (P : Set a) (Q : Set b) → F P Q → Q)
    → {a b c : Level}
    → (X : Set a) (Y : Set b) (Z : Set c)
    → (X → Y → Z)
    → (F X Y → Z)
  uncurry F p1 p2 X Y Z f d = f (p1 X Y d) (p2 X Y d)

  data And′ {a b : Level} : Set a → Set b → Set (a ⊔ b) where
    and : (X : Set a) → (Y : Set b) → X → Y → And′ X Y

  curryAnd
    : {a b c : Level}
    → (X : Set a) (Y : Set b) (Z : Set c)
    → (And′ X Y → Z)
    → (X → Y → Z)
  curryAnd X Y Z f x y = f (and X Y x y)

  uncurryAnd
    : {a b c : Level}
    → (X : Set a) (Y : Set b) (Z : Set c)
    → (X → Y → Z)
    → (And′ X Y → Z)
  uncurryAnd = uncurry And′ p1 p2 where
    p1 : {a b : Level} (P : Set a) (Q : Set b) → (And′ P Q) → P
    p1 P Q (and .P .Q p q) = p

    p2 : {a b : Level} (P : Set a) (Q : Set b) → (And′ P Q) → Q
    p2 P Q (and .P .Q p q) = q