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

Определение

Для функции двух аргументов ${\displaystyle h\colon (A\times B)\to C}$ , оператор каррирования ${\displaystyle \Lambda }$ выполняет преобразование ${\displaystyle h}$ в функцию ${\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 — сопряжённые функторы.

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

С точки зрения соответствия Карри — Ховарда существование функций каррирования (обитаемость типа ${\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 // . — Princeton : Institute for Advanced Study , 2013. — 603 p.