Введение

Преобразование функции таким образом, чтобы она принимала только один аргумент – это математическая техника. В математике и информатике, каррирование – это техника преобразования функции, принимающей несколько аргументов, в последовательность семейств функций, каждое из которых принимает один аргумент. В типичном примере начинают с функции, принимающей два аргумента, один из множества A и один из множества B, и возвращающей объекты из множества C. Карированная форма этой функции рассматривает первый аргумент как параметр, чтобы создать семейство функций. Это семейство организовано таким образом, что для каждого объекта a из множества A существует ровно одна функция.

В этом примере сама функция становится функцией, принимающей a в качестве аргумента и возвращающей функцию, которая отображает каждый элемент b из B в элемент из C. Строгое обозначение для выражения этого довольно громоздко. Функция f принадлежит множеству функций A → C. При этом функция f(a) принадлежит множеству функций B → C. Таким образом, отображение из A в B будет иметь тип A → (B → C). С этим обозначением f – это функция, которая принимает объекты из множества A и возвращает объекты из множества функций B → C, и поэтому записывается как f(a). Это несколько неформальный пример; более точные определения понятий "объект" и "функция" приведены ниже. Эти определения варьируются в зависимости от контекста и принимают различные формы в зависимости от используемой теории. Каррирование связано с частичным применением, но не является им. Разработано Мозесом Шенфинкелем и далее развито Хаскеллом Карри. Uncurrying – это двойственное преобразование к каррированию и может рассматриваться как форма дефункционализации. Оно принимает функцию, возвращающую другую функцию, и выдает новую функцию, которая принимает в качестве параметров аргументы для обеих функций и возвращает, в результате, применение первой функции, а затем второй, к этим аргументам. Этот процесс можно повторять.

Мотивация

Каррирование предоставляет способ работы с функциями, принимающими несколько аргументов, и их использования в средах, где функции могут принимать только один аргумент. Например, некоторые аналитические методы применимы только к функциям с одним аргументом. Практические функции часто принимают больше аргументов, чем это требуется. Фреге показал, что достаточно предоставить решения для случая с одним аргументом, поскольку функцию с несколькими аргументами можно преобразовать в цепочку функций с одним аргументом. Это преобразование и есть процесс, известный как каррирование. Все "обычные" функции, встречающиеся в математическом анализе или в программировании, могут быть карированы. Однако существуют категории, в которых каррирование невозможно; наиболее общими категориями, допускающими каррирование, являются замкнутые моноидальные категории. Некоторые языки программирования почти всегда используют карированные функции для работы с несколькими аргументами; примечательными примерами являются ML и Haskell, где во всех случаях функции имеют ровно один аргумент. Это свойство унаследовано от лямбда-исчисления, где функции с несколькими аргументами обычно представляются в карированной форме. Каррирование связано с, но не идентично частичному применению функции. Предложено альтернативное название – "Шёнфинкелизация". В математическом контексте принцип восходит к работам Фреге 1893 года. Однако, хотя концепция упоминается, и Карри упоминается в контексте функций высшего порядка, слово "currying" не встречается в его записях, и Карри не ассоциируется с этой концепцией, хотя примеров больше. Одним из полезных следствий является то, что функция непрерывна тогда и только тогда, когда её карированная форма непрерывна. Другой важный результат заключается в том, что карта применения, обычно называемая "вычислением" в данном контексте, является непрерывной (стоит отметить, что eval – это принципиально иное понятие в информатике). То есть, является непрерывной, когда компактно открыто и локально компактно хаусдорфово. Эти два результата имеют ключевое значение для установления непрерывности гомотопии, то есть когда является единичным интервалом, так что можно рассматривать как гомотопию двух функций из в , или, эквивалентно, как один (непрерывный) путь в .

Алгебраическая топология

В алгебраической топологии каррирование служит примером дуальности Экманна — Хилтона и, как следствие, играет важную роль в различных областях. Например, пространство петли сопряжено к редуцированным подвескам; это обычно записывается как

где — множество классов гомотопии отображений , — подвеска A, а — пространство петли A. По сути, подвеску можно рассматривать как декартово произведение с единичным интервалом, наложенное отношение эквивалентности, превращающее интервал в петлю. Каррированная форма отображает пространство в пространство функций из петли в , то есть из в Скотт-непрерывные функции. Скотт-непрерывные функции впервые были исследованы в попытке предоставить семантику для лямбда-исчисления (поскольку обычная теория множеств для этого не подходит). В более общем плане функции Скотта изучаются в теории доменов, которая охватывает изучение денотационной семантики компьютерных алгоритмов. Следует отметить, что топология Скотта существенно отличается от многих распространенных топологий, встречающихся в категории топологических пространств; топология Скотта обычно тоньше и не является трезвой. Понятие непрерывности появляется в гомотопической теории типов, где, грубо говоря, две компьютерные программы можно считать гомотопичными, то есть вычисляющими одни и те же результаты, если их можно «непрерывно» рефакторировать друг в друга.

Ламбда калькули

В теоретической информатике каррирование предоставляет способ изучения функций с несколькими аргументами в очень простых теоретических моделях, таких как лямбда-исчисление, в которых функции принимают только один аргумент. Рассмотрим функцию, принимающую два аргумента и имеющую тип , что означает, что x должен иметь тип , y должен иметь тип , а сама функция возвращает тип . Карированная форма f определяется как , где – абстрактор лямбда-исчисления. Поскольку curry принимает в качестве входных данных функции с типом , можно заключить, что тип самой функции curry равен . Оператор → часто рассматривается как правоассоциативный, поэтому карированный тип функции часто записывается как . И наоборот, применение функции считается левоассоциативным, так что эквивалентно . То есть, скобки не нужны для уточнения порядка применения. Карированные функции могут использоваться в любом языке программирования, поддерживающем замыкания; однако некарированные функции обычно предпочтительнее из соображений эффективности, поскольку в большинстве случаев вызовов функций можно избежать накладных расходов, связанных с частичным применением и созданием замыканий.

Теория типов

В теории типов общая идея системы типов в информатике формализуется в конкретную алгебру типов. Например, когда записывают , подразумевается, что и являются типами, а стрелка – конструктор типа, в частности, функциональный тип или тип-стрелка. Аналогично, декартово произведение типов строится с помощью конструктора типа произведения . Теоретико-типовой подход находит отражение в языках программирования, таких как ML, а также в языках, произошедших от него или вдохновленных им: CaML, Haskell и F#. Этот подход обеспечивает естественное дополнение к языку теории категорий, как будет обсуждаться ниже. Это связано с тем, что категории, и особенно моноидальные категории, обладают внутренним языком, наиболее ярким примером которого является просто типизированное лямбда-исчисление. Это важно в данном контексте, поскольку его можно построить на основе единственного конструктора типа – типа-стрелки. Каррирование затем наделяет язык естественным типом произведения. Соответствие между объектами в категориях и типами позволяет интерпретировать языки программирования как логики (через соответствие Карри — Ховарда), а также как другие типы математических систем, что будет рассмотрено далее.

Логика

В соответствии с соответствием Карри-Ховарда, существование каррирования и ан-каррирования эквивалентно логической теореме, поскольку кортежи (тип-произведение) соответствует конъюнкции в логике, а функциональный тип – импликации. Экспоненциальный объект в категории алгебр Хейтинга обычно записывается как материальная импликация. Дистрибутивные алгебры Хейтинга являются булевыми алгебрами, а экспоненциальный объект имеет вид , что наглядно демонстрирует, что экспоненциальный объект действительно является материальной импликацией.

Контраст с частичным применением функции

Каррирование и частичное применение функции часто смешиваются. Одним из существенных различий между ними является то, что вызов частично примененной функции возвращает результат немедленно, а не другую функцию в цепочке каррирования; это различие особенно заметно для функций с арностью больше двух. Для функции типа , каррирование создает функцию типа , то есть, если вычисление первой функции можно представить как , то вычисление каррированной функции будет представлено как , последовательно применяя каждый аргумент к функции одного аргумента, возвращаемой предыдущим вызовом. Обратите внимание, что после вызова , у нас остается функция, принимающая один аргумент и возвращающая другую функцию, а не функцию, принимающую два аргумента. В отличие от этого, частичное применение функции — это процесс фиксации некоторого числа аргументов функции, в результате чего получается другая функция с меньшей арностью. Учитывая определение выше, мы можем зафиксировать (или «связать») первый аргумент, получив функцию типа . Вычисление этой функции можно представить как . Обратите внимание, что результат частичного применения в этом случае — это функция, принимающая два аргумента. Интуитивно, частичное применение функции говорит: «если вы фиксируете первый аргумент функции, вы получаете функцию, работающую с оставшимися аргументами». Например, если функция `div` обозначает операцию деления x/y, то `div` с параметром x, фиксированным на 1 (т. е. `div 1`) — это другая функция: эквивалентная функции `inv`, которая возвращает мультипликативную обратную величину своего аргумента, определяемую как `inv(y) = 1/y`. Практическая мотивация для частичного применения заключается в том, что функции, полученные путем передачи лишь части аргументов функции, часто оказываются полезными; например, во многих языках есть функция или оператор, аналогичный «прибавить один». Частичное применение позволяет легко определять такие функции, например, создавая функцию, представляющую оператор сложения с 1, зафиксированным в качестве первого аргумента. Частичное применение можно рассматривать как вычисление каррированной функции в фиксированной точке, например, для заданных и , получаем или просто , где каррирует первый параметр `f`. Таким образом, частичное применение сводится к каррированной функции в фиксированной точке. Более того, каррированная функция в фиксированной точке (тривиально) является частичным применением. В качестве дополнительного доказательства отметим, что для любой функции можно определить функцию таким образом, что любое частичное применение можно свести к единственной операции каррирования. Следовательно, каррирование более уместно определять как операцию, которая во многих теоретических случаях часто применяется рекурсивно, но которая теоретически неотличима (при рассмотрении как операция) от частичного применения. Таким образом, частичное применение можно определить как объективный результат однократного применения оператора каррирования к некоторому порядку входных данных функции.