Interested Article - Каррирование

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

Определение

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

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

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

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

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

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

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

Каррирование с точки зрения программирования

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

В языках программирования с функциями первого класса обычно определены операции 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, « от 15 мая 2013 на Wayback Machine », (2009) от 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 // . — Princeton : Institute for Advanced Study , 2013. — 603 p.
Источник —

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