Init.Data.Function

Function.curry definition

: (α × β → φ) → α → β → φ

Full source

/--
Transforms a function from pairs into an equivalent two-parameter function.

Examples:
 * `Function.curry (fun (x, y) => x + y) 3 5 = 8`
 * `Function.curry Prod.swap 3 "five" = ("five", 3)`
-/
@[inline]
def curry : (α × β → φ) → α → β → φ := fun f a b => f (a, b)

Currying a function on pairs

Informal description

The function `Function.curry` transforms a function $f : \alpha \times \beta \to \phi$ defined on pairs into a two-parameter function $g : \alpha \to \beta \to \phi$ such that for any $a \in \alpha$ and $b \in \beta$, $g(a)(b) = f(a, b)$. For example: - If $f(x, y) = x + y$, then $\text{curry}(f)(3)(5) = 8$. - If $f = \text{Prod.swap}$, then $\text{curry}(f)(3)(\text{"five"}) = (\text{"five"}, 3)$.

Function.uncurry definition

: (α → β → φ) → α × β → φ

Full source

/--
Transforms a two-parameter function into an equivalent function from pairs.

Examples:
 * `Function.uncurry List.drop (1, ["a", "b", "c"]) = ["b", "c"]`
 * `[("orange", 2), ("android", 3) ].map (Function.uncurry String.take) = ["or", "and"]`
-/
@[inline]
def uncurry : (α → β → φ) → α × β → φ := fun f a => f a.1 a.2

Uncurrying a two-parameter function

Informal description

The function `Function.uncurry` takes a two-parameter function $f : \alpha \to \beta \to \phi$ and returns a function $g : \alpha \times \beta \to \phi$ such that for any pair $(a, b) \in \alpha \times \beta$, $g(a, b) = f(a)(b)$. This transformation allows a two-parameter function to be applied to ordered pairs directly.

Function.curry_uncurry theorem

(f : α → β → φ) : curry (uncurry f) = f

Full source

@[simp]
theorem curry_uncurry (f : α → β → φ) : curry (uncurry f) = f :=
  rfl

Currying and Uncurrying Preserves Identity: $\operatorname{curry} \circ \operatorname{uncurry} = \mathrm{id}$

Informal description

For any function $f \colon \alpha \to \beta \to \phi$, the composition of currying and uncurrying returns the original function, i.e., $\operatorname{curry}(\operatorname{uncurry}(f)) = f$.

Function.uncurry_curry theorem

(f : α × β → φ) : uncurry (curry f) = f

Full source

@[simp]
theorem uncurry_curry (f : α × β → φ) : uncurry (curry f) = f :=
  funext fun ⟨_a, _b⟩ => rfl

Uncurrying and Currying Preserves Identity: $\operatorname{uncurry} \circ \operatorname{curry} = \mathrm{id}$

Informal description

For any function $f \colon \alpha \times \beta \to \phi$, the composition of uncurrying and currying returns the original function, i.e., $\operatorname{uncurry}(\operatorname{curry}(f)) = f$.

Function.uncurry_apply_pair theorem

{α β γ} (f : α → β → γ) (x : α) (y : β) : uncurry f (x, y) = f x y

Full source

@[simp]
theorem uncurry_apply_pair {α β γ} (f : α → β → γ) (x : α) (y : β) : uncurry f (x, y) = f x y :=
  rfl

Uncurrying a Function Evaluated at a Pair Equals the Original Function Applied to the Components

Informal description

For any function $f \colon \alpha \to \beta \to \gamma$ and any elements $x \in \alpha$, $y \in \beta$, the uncurried version of $f$ satisfies $\operatorname{uncurry}(f)(x, y) = f(x)(y)$.

Function.curry_apply theorem

{α β γ} (f : α × β → γ) (x : α) (y : β) : curry f x y = f (x, y)

Full source

@[simp]
theorem curry_apply {α β γ} (f : α × β → γ) (x : α) (y : β) : curry f x y = f (x, y) :=
  rfl

Currying a Function Preserves Evaluation

Informal description

For any function $f \colon \alpha \times \beta \to \gamma$ and any elements $x \in \alpha$, $y \in \beta$, the curried version of $f$ satisfies $\operatorname{curry}(f)(x)(y) = f(x, y)$.