Currying and uncurrying of n-ary functions

A function of n arguments can either be written as f a₁ a₂ ⋯ aₙ or f' ![a₁, a₂, ⋯, aₙ]. This file provides the currying and uncurrying operations that convert between the two, as n-ary generalizations of the binary curry and uncurry.

Main definitions

• Function.OfArity.uncurry: convert an n-ary function to a function from Fin n → α.
• Function.OfArity.curry: convert a function from Fin n → α to an n-ary function.
• Function.FromTypes.uncurry: convert an p-ary heterogeneous function to a function from (i : Fin n) → p i.
• Function.FromTypes.curry: convert a function from (i : Fin n) → p i to a p-ary heterogeneous function.

def Function.FromTypes.uncurry {n : ℕ} {p : Fin n → Type u} {τ : Type u} (f : Function.FromTypes p τ) : ((i : Fin n) → p i) → τ

Uncurry all the arguments of Function.FromTypes p τ to get a function from a tuple.

Note this can be used on raw functions if used.

Equations

• Function.FromTypes.uncurry x = fun (x_1 : (i : Fin 0) → x_4 i) => x
• Function.FromTypes.uncurry x = fun (args : (i : Fin (n + 1)) → x_4 i) => Function.FromTypes.uncurry (x (args 0)) ((fun {x : Fin n} => args) ∘' Fin.succ)

def Function.FromTypes.curry {n : ℕ} {p : Fin n → Type u} {τ : Type u} : (((i : Fin n) → p i) → τ) → Function.FromTypes p τ

Curry all the arguments of Function.FromTypes p τ to get a function from a tuple.

Equations

• Function.FromTypes.curry x = x fun (a : Fin 0) => isEmptyElim a
• Function.FromTypes.curry x = fun (a : Matrix.vecHead x_4) => Function.FromTypes.curry fun (args : (i : Fin (Nat.add n 0)) → Matrix.vecTail x_4 i) => x (Fin.cons a args)

@[simp]

theorem Function.FromTypes.uncurry_apply_cons {n : ℕ} {α : Type u} {p : Fin n → Type u} {τ : Type u} (f : Function.FromTypes (Matrix.vecCons α p) τ) (a : α) (args : (i : Fin n) → p i) : Function.FromTypes.uncurry f (Fin.cons a args) = Function.FromTypes.uncurry (f a) args

@[simp]

theorem Function.FromTypes.uncurry_apply_succ {n : ℕ} {p : Fin (n + 1) → Type u} {τ : Type u} (f : Function.FromTypes p τ) (args : (i : Fin (n + 1)) → p i) : Function.FromTypes.uncurry f args = Function.FromTypes.uncurry (f (args 0)) (Fin.tail args)

@[simp]

theorem Function.FromTypes.curry_apply_cons {n : ℕ} {α : Type u} {p : Fin n → Type u} {τ : Type u} (f : ((i : Fin (n + 1)) → Matrix.vecCons α p i) → τ) (a : α) : Function.FromTypes.curry f a = Function.FromTypes.curry ((fun {x : (i : Fin n) → Matrix.vecCons α p (Fin.succ i)} => f) ∘' Fin.cons a)

@[simp]

theorem Function.FromTypes.curry_apply_succ {n : ℕ} {p : Fin (n + 1) → Type u} {τ : Type u} (f : ((i : Fin (n + 1)) → p i) → τ) (a : p 0) : Function.FromTypes.curry f a = Function.FromTypes.curry (f ∘ Fin.cons a)

@[simp]

theorem Function.FromTypes.curry_uncurry {n : ℕ} {p : Fin n → Type u} {τ : Type u} (f : Function.FromTypes p τ) : Function.FromTypes.curry (Function.FromTypes.uncurry f) = f

@[simp]

theorem Function.FromTypes.uncurry_curry {n : ℕ} {p : Fin n → Type u} {τ : Type u} (f : ((i : Fin n) → p i) → τ) : Function.FromTypes.uncurry (Function.FromTypes.curry f) = f

@[simp]

theorem Function.FromTypes.curryEquiv_apply {n : ℕ} {τ : Type u} (p : Fin n → Type u) : ∀ (a : ((i : Fin n) → p i) → τ), (Function.FromTypes.curryEquiv p) a = Function.FromTypes.curry a

@[simp]

theorem Function.FromTypes.curryEquiv_symm_apply {n : ℕ} {τ : Type u} (p : Fin n → Type u) (f : Function.FromTypes p τ) : ∀ (a : (i : Fin n) → p i), (Function.FromTypes.curryEquiv p).symm f a = Function.FromTypes.uncurry f a

def Function.FromTypes.curryEquiv {n : ℕ} {τ : Type u} (p : Fin n → Type u) : (((i : Fin n) → p i) → τ) ≃ Function.FromTypes p τ

Equiv.curry for p-ary heterogeneous functions.

Equations

• Function.FromTypes.curryEquiv p = { toFun := Function.FromTypes.curry, invFun := Function.FromTypes.uncurry, left_inv := ⋯, right_inv := ⋯ }

theorem Function.FromTypes.curry_two_eq_curry {p : Fin 2 → Type u} {τ : Type u} (f : ((i : Fin 2) → p i) → τ) : Function.FromTypes.curry f = Function.curry (f ∘ ⇑(piFinTwoEquiv p).symm)

theorem Function.FromTypes.uncurry_two_eq_uncurry (p : Fin 2 → Type u) (τ : Type u) (f : Function.FromTypes p τ) : Function.FromTypes.uncurry f = Function.uncurry f ∘ ⇑(piFinTwoEquiv p)

def Function.OfArity.uncurry {α : Type u} {β : Type u} {n : ℕ} (f : Function.OfArity α β n) : (Fin n → α) → β

Uncurry all the arguments of Function.OfArity α n to get a function from a tuple.

Note this can be used on raw functions if used.

Equations

• Function.OfArity.uncurry f = Function.FromTypes.uncurry f

def Function.OfArity.curry {α : Type u} {β : Type u} {n : ℕ} (f : (Fin n → α) → β) : Function.OfArity α β n

Curry all the arguments of Function.OfArity α β n to get a function from a tuple.

Equations

• Function.OfArity.curry f = Function.FromTypes.curry f

@[simp]

theorem Function.OfArity.curry_uncurry {α : Type u} {β : Type u} {n : ℕ} (f : Function.OfArity α β n) : Function.OfArity.curry (Function.OfArity.uncurry f) = f

@[simp]

theorem Function.OfArity.uncurry_curry {α : Type u} {β : Type u} {n : ℕ} (f : (Fin n → α) → β) : Function.OfArity.uncurry (Function.OfArity.curry f) = f

@[simp]

theorem Function.OfArity.curryEquiv_apply {α : Type u} {β : Type u} (n : ℕ) : ∀ (a : ((i : Fin n) → (fun (a : Fin n) => α) i) → β), (Function.OfArity.curryEquiv n) a = Function.FromTypes.curry a

@[simp]

theorem Function.OfArity.curryEquiv_symm_apply {α : Type u} {β : Type u} (n : ℕ) (f : Function.FromTypes (fun (a : Fin n) => α) β) : ∀ (a : Fin n → α), (Function.OfArity.curryEquiv n).symm f a = Function.FromTypes.uncurry f a

def Function.OfArity.curryEquiv {α : Type u} {β : Type u} (n : ℕ) : ((Fin n → α) → β) ≃ Function.OfArity α β n

Equiv.curry for n-ary functions.

Equations

• Function.OfArity.curryEquiv n = Function.FromTypes.curryEquiv fun (a : Fin n) => α

theorem Function.OfArity.curry_two_eq_curry {α : Type u} {β : Type u} (f : (Fin 2 → α) → β) : Function.OfArity.curry f = Function.curry (f ∘ ⇑(finTwoArrowEquiv α).symm)

theorem Function.OfArity.uncurry_two_eq_uncurry {α : Type u} {β : Type u} (f : Function.OfArity α β 2) : Function.OfArity.uncurry f = Function.uncurry f ∘ ⇑(finTwoArrowEquiv α)