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

Материал из Википедии — свободной энциклопедии
Перейти к навигации Перейти к поиску

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

Определение[править | править код]

Для функции двух аргументов , оператор каррирования выполняет преобразование в функцию , которая берёт аргумент типа и возвращает функцию типа . С интуитивной точки зрения, каррирование функции позволяет фиксировать её некоторый аргумент, возвращая функцию от остальных аргументов. Таким образом,  — функция типа .

Декаррирование (англ. uncurring) вводится как обратное преобразование, восстанавливающее каррированный аргумент: для функции оператор декаррирования выполняет преобразование в ; тип оператора декаррирования — .

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

Математическая точка зрения[править | править код]

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

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

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

Каррирование с точки зрения программирования[править | править код]

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

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

Примечания[править | править код]

  1. John c. Baez and Mike Stay, «Physics, Topology, Logic and Computation: A Rosetta Stone Архивная копия от 15 мая 2013 на Wayback Machine», (2009) ArXiv 0903.0340 Архивная копия от 20 июля 2014 на Wayback Machine in New Structures for Physics, ed. Bob Coecke, Lecture Notes in Physics vol. 813, Springer, Berlin, 2011, p. 95—174.

Литература[править | править код]

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