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

Каррирование или карринг (англ. currying) в информатике — преобразование функции от многих аргументов в набор функций, каждая из которых является функцией от одного аргумента. Возможность такого преобразования впервые отмечена в трудах Готтлоба Фреге, систематически изучена Моисеем Шейнфинкелем в 1920-е годы, а наименование получило по имени Хаскелла Карри — разработчика комбинаторной логики, в которой сведение к функциям одного аргумента носит основополагающий характер.

Определение

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

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

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

Математическая точка зрения

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

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

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

Литература

• Бенджамин Пирс. Типы в языках программирования / Пер. с англ.: Г. Бронников, А. Отт. — Добросвет, 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.