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

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

Определение

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

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

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

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

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

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

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

Литература

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

Отрывок, характеризующий Каррирование

– Приехали. Жюли Друбецкая говорила мне. Я поехал к ним и не застал. Они уехали в подмосковную.


Офицеры хотели откланяться, но князь Андрей, как будто не желая оставаться с глазу на глаз с своим другом, предложил им посидеть и напиться чаю. Подали скамейки и чай. Офицеры не без удивления смотрели на толстую, громадную фигуру Пьера и слушали его рассказы о Москве и о расположении наших войск, которые ему удалось объездить. Князь Андрей молчал, и лицо его так было неприятно, что Пьер обращался более к добродушному батальонному командиру Тимохину, чем к Болконскому.
– Так ты понял все расположение войск? – перебил его князь Андрей.
– Да, то есть как? – сказал Пьер. – Как невоенный человек, я не могу сказать, чтобы вполне, но все таки понял общее расположение.
– Eh bien, vous etes plus avance que qui cela soit, [Ну, так ты больше знаешь, чем кто бы то ни было.] – сказал князь Андрей.
– A! – сказал Пьер с недоуменьем, через очки глядя на князя Андрея. – Ну, как вы скажете насчет назначения Кутузова? – сказал он.
– Я очень рад был этому назначению, вот все, что я знаю, – сказал князь Андрей.
– Ну, а скажите, какое ваше мнение насчет Барклая де Толли? В Москве бог знает что говорили про него. Как вы судите о нем?
– Спроси вот у них, – сказал князь Андрей, указывая на офицеров.
Пьер с снисходительно вопросительной улыбкой, с которой невольно все обращались к Тимохину, посмотрел на него.
– Свет увидали, ваше сиятельство, как светлейший поступил, – робко и беспрестанно оглядываясь на своего полкового командира, сказал Тимохин.
– Отчего же так? – спросил Пьер.
– Да вот хоть бы насчет дров или кормов, доложу вам. Ведь мы от Свенцян отступали, не смей хворостины тронуть, или сенца там, или что. Ведь мы уходим, ему достается, не так ли, ваше сиятельство? – обратился он к своему князю, – а ты не смей. В нашем полку под суд двух офицеров отдали за этакие дела. Ну, как светлейший поступил, так насчет этого просто стало. Свет увидали…
– Так отчего же он запрещал?
Тимохин сконфуженно оглядывался, не понимая, как и что отвечать на такой вопрос. Пьер с тем же вопросом обратился к князю Андрею.
– А чтобы не разорять край, который мы оставляли неприятелю, – злобно насмешливо сказал князь Андрей. – Это очень основательно; нельзя позволять грабить край и приучаться войскам к мародерству. Ну и в Смоленске он тоже правильно рассудил, что французы могут обойти нас и что у них больше сил. Но он не мог понять того, – вдруг как бы вырвавшимся тонким голосом закричал князь Андрей, – но он не мог понять, что мы в первый раз дрались там за русскую землю, что в войсках был такой дух, какого никогда я не видал, что мы два дня сряду отбивали французов и что этот успех удесятерял наши силы. Он велел отступать, и все усилия и потери пропали даром. Он не думал об измене, он старался все сделать как можно лучше, он все обдумал; но от этого то он и не годится. Он не годится теперь именно потому, что он все обдумывает очень основательно и аккуратно, как и следует всякому немцу. Как бы тебе сказать… Ну, у отца твоего немец лакей, и он прекрасный лакей и удовлетворит всем его нуждам лучше тебя, и пускай он служит; но ежели отец при смерти болен, ты прогонишь лакея и своими непривычными, неловкими руками станешь ходить за отцом и лучше успокоишь его, чем искусный, но чужой человек. Так и сделали с Барклаем. Пока Россия была здорова, ей мог служить чужой, и был прекрасный министр, но как только она в опасности; нужен свой, родной человек. А у вас в клубе выдумали, что он изменник! Тем, что его оклеветали изменником, сделают только то, что потом, устыдившись своего ложного нарекания, из изменников сделают вдруг героем или гением, что еще будет несправедливее. Он честный и очень аккуратный немец…
– Однако, говорят, он искусный полководец, – сказал Пьер.
– Я не понимаю, что такое значит искусный полководец, – с насмешкой сказал князь Андрей.
– Искусный полководец, – сказал Пьер, – ну, тот, который предвидел все случайности… ну, угадал мысли противника.
– Да это невозможно, – сказал князь Андрей, как будто про давно решенное дело.
Пьер с удивлением посмотрел на него.
– Однако, – сказал он, – ведь говорят же, что война подобна шахматной игре.
– Да, – сказал князь Андрей, – только с тою маленькою разницей, что в шахматах над каждым шагом ты можешь думать сколько угодно, что ты там вне условий времени, и еще с той разницей, что конь всегда сильнее пешки и две пешки всегда сильнее одной, a на войне один батальон иногда сильнее дивизии, а иногда слабее роты. Относительная сила войск никому не может быть известна. Поверь мне, – сказал он, – что ежели бы что зависело от распоряжений штабов, то я бы был там и делал бы распоряжения, а вместо того я имею честь служить здесь, в полку вот с этими господами, и считаю, что от нас действительно будет зависеть завтрашний день, а не от них… Успех никогда не зависел и не будет зависеть ни от позиции, ни от вооружения, ни даже от числа; а уж меньше всего от позиции.