Каррирование

Для функции двух аргументов ${\displaystyle h\colon (A\times B)\to C}$ оператор каррирования ${\displaystyle \Lambda }$ выполняет преобразование ${\displaystyle \Lambda (h)\colon A\to (B\to C)}$ — берёт аргумент типа ${\displaystyle A}$ и возвращает функцию типа ${\displaystyle (B\to C)}$. С интуитивной точки зрения, каррирование функции позволяет фиксировать её некоторый аргумент, возвращая функцию от остальных аргументов. Таким образом, ${\displaystyle \Lambda }$ — функция типа ${\displaystyle (A\times B\to C)\to (A\to (B\to C))}$.

Декаррирование (англ. uncurring) вводится как обратное преобразование — восстанавливающее каррированный аргумент: для функции ${\displaystyle k\colon A\to (B\to C)}$ оператор декаррирования ${\displaystyle \epsilon }$ выполняет преобразование ${\displaystyle \epsilon (k)\colon A\times B\to C}$; тип оператора декаррирования — ${\displaystyle (A\to (B\to C))\to (A\times B\to C)}$.

На практике каррирование позволяет рассматривать функцию, которая получила не все из предусмотренных аргументов. Оператор каррирования встроен в некоторые языки программирования, что позволяет многоместные функции приводить к каррированному представлению, наиболее характерные примеры таких языков — ML и Haskell. Все языки, поддерживающие замыкание, позволяют записывать каррированные функции.

В теоретической информатике каррирование предоставляет способ изучения функций нескольких аргументов в рамках очень простых теоретических систем, таких как лямбда-исчисление. В рамках теории множеств каррирование — это соответствие между множествами ${\displaystyle C^{A\times B}}$ и ${\displaystyle \left(C^{B}\right)^{A}}$. В теории категорий каррирование появляется благодаря универсальному свойству экспоненциала; в ситуации декартово замкнутой категории это приводит к следующему соответствию. Существует биекция между множествами морфизмов из бинарного произведения ${\displaystyle f\colon (X\times Y)\to Z}$ и морфизмами в экспоненциал ${\displaystyle g\colon X\to Z^{Y}}$, которая естественна по ${\displaystyle X}$ и по ${\displaystyle Z}$. Это утверждение эквивалентно тому, что функтор произведения и функтор Hom — сопряжённые функторы.

Это является ключевым свойством декартово замкнутой категории, или, более общей, замкнутой моноидальной категории. Первой вполне достаточно для классической логики, однако вторая является удобной теоретической основой для квантовых вычислений. Различие состоит в том, что декартово произведение содержит только информацию о паре двух объектов, тогда как тензорное произведение, используемое в определении моноидальной категории, подходит для описания запутанных состояний[1].

С точки зрения соответствия Карри — Ховарда существование функций каррирования (обитаемость типа ${\displaystyle ((A\times B)\to C)\to (A\to (B\to C)}$ и декаррирования (обитаемость типа ${\displaystyle (A\to (B\to C)\to ((A\times B)\to C)}$) эквивалентно логическому утверждению ${\displaystyle ((A\land B)\Rightarrow C)\Leftrightarrow (A\Rightarrow (B\Rightarrow C))}$ (тип-произведение ${\displaystyle A\times B}$ соответствует конъюнкции, а функциональный тип ${\displaystyle A\to B}$ — импликации). Функции каррирования и декаррирования непрерывны по Скотту.

Каррирование широко используется в языках программирования, прежде всего, поддерживающих парадигму функционального программирования. В некоторых языках функции каррированы по умолчанию, то есть, многоместные функции реализуются как одноместные функции высших порядков, а применение аргументов к ним — как последовательность частичных применений.

В языках программирования с функциями первого класса обычно определены операции curry (переводящая функцию сигнатуры вида A, B -> C в функцию сигнатуры A -> B -> C) и uncurry (осуществляющее обратное преобразование — ставящая в соответствие функции сигнатуры вида A -> B -> C двуместную функцию вида A, B -> C). В этих случаях прозрачна связь с операцией частичного применения papply: curry papply = curry.

• Бенджамин Пирс. Типы в языках программирования / Пер. с англ.: Г. Бронников, А. Отт. — Добросвет, 2011. — С. 76. — 656 с. — ISBN 978-5-7913-0082-9.
• Type theory // Homotopy Type Theory: Univalent Foundations of Mathematics. — Princeton: Institute for Advanced Study, 2013. — 603 p.