Стрелка (компьютерные науки)

В информатике стрелки или болты — это класс типов, используемый в программировании для описания вычислений в чистом и декларативном виде. Впервые предложенные ученым-компьютерщиком Джоном Хьюзом в качестве обобщения монад , стрелки предоставляют ссылочно прозрачный способ выражения отношений между логическими шагами в вычислении. ^[1] В отличие от монад, стрелки не ограничивают шаги наличием одного и только одного входа. В результате они нашли применение в функциональном реактивном программировании , программировании без точек и парсерах среди других приложений. ^{[1] [2]}

Хотя стрелки использовались до того, как были признаны отдельным классом, только в 2000 году Джон Хьюз впервые опубликовал исследование, посвященное им. До этого монады были достаточны для большинства задач, требующих объединения программной логики в чистом коде. Однако некоторые полезные библиотеки , такие как библиотека Fudgets для графических пользовательских интерфейсов и некоторые эффективные парсеры, не поддавались переписыванию в монадической форме. ^[1]

Формальная концепция стрелок была разработана для объяснения этих исключений из монадического кода, и в ходе этого процесса сами монады оказались подмножеством стрелок . ^[1] С тех пор стрелки стали активной областью исследований. Их основные законы и операции были уточнены несколько раз, и недавние формулировки, такие как исчисление стрелок, требуют всего пяти законов. ^[3]

В теории категорий категории Клейсли всех монад образуют собственное подмножество стрелок Хьюза. ^[1] Хотя некоторое время считалось, что категории Фрейда эквивалентны стрелкам, ^[4] с тех пор было доказано, что стрелки являются даже более общими. Фактически, стрелки не просто эквивалентны, но и прямо равны обогащенным категориям Фрейда. ^[5]

Как и все классы типов, стрелки можно рассматривать как набор качеств, которые могут быть применены к любому типу данных . В языке программирования Haskell стрелки позволяют функциям (представленным в Haskell ->символом) объединяться в овеществленную форму. Однако фактический термин «стрелка» может также исходить из того факта, что некоторые (но не все) стрелки соответствуют морфизмам ( также известным как «стрелки» в теории категорий) различных категорий Клейсли. Как относительно новая концепция, не существует единого стандартного определения, но все формулировки логически эквивалентны, содержат некоторые требуемые методы и строго подчиняются определенным математическим законам. ^[6]

Описание, используемое в настоящее время стандартными библиотеками Haskell, требует только трех основных операций:

• Конструктор типа arr , который переводит функции -> из любого типа s в другой t и поднимает эти функции в стрелку A между двумя типами. ^[7]

обр : ( с -> т ) -> А с т        

• Метод конвейеризации сначала берет стрелку между двумя типами и преобразует ее в стрелку между кортежами . Первые элементы в кортежах представляют часть ввода и вывода, которая изменяется, в то время как вторые элементы являются третьим типом u, описывающим неизмененную часть, которая обходит вычисления. ^[7]

первый : A s t -> A ( s , u ) ( t , u )        

• Поскольку все стрелки должны быть категориями , они наследуют третью операцию из класса категорий: оператор композиции >>> , который может присоединить вторую стрелку к первой, если выходные данные первой функции и входные данные второй имеют совпадающие типы. ^[7]

( >>> ) : А с т -> А т у -> А с у            

Хотя для определения стрелки строго необходимы только эти три процедуры, можно разработать и другие методы, которые упростят работу со стрелками на практике и в теории.

Еще один полезный метод можно вывести из arr и first (и из которого можно вывести first ):

• Оператор слияния ***, который берет две стрелки, возможно с разными входными и выходными типами, и объединяет их в одну стрелку между двумя составными типами. Оператор слияния не обязательно коммутативен . ^[7]

( *** ) : А с т -> А у в -> А ( с , у ) ( т , в )            

Помимо наличия некоторых четко определенных процедур, стрелки должны подчиняться определенным правилам для любых типов, к которым они могут применяться:

• Стрелки всегда должны сохранять идентификаторы всех типов (по сути, определения всех значений для всех типов в пределах категории). ^[7 ]

идентификатор обр == идентификатор   

• При соединении двух функций f и g требуемые операции со стрелками должны распределяться по композициям слева направо. ^[7]

arr ( f >>> g ) == arr f >>> arr g первый ( f >>> g ) == первый f >>> первый g                  

• В предыдущих законах трубопроводы можно было напрямую применять к функциям, поскольку порядок не имел значения, когда трубопроводы и подъем выполнялись одновременно. ^[7]

arr ( первая f ) == первая ( arr f )      

Остальные законы ограничивают поведение метода трубной обвязки при изменении порядка композиции на обратный, что также позволяет упростить выражения :

• Если идентификатор объединяется со второй функцией для формирования стрелки, присоединение его к конвейерной функции должно быть коммутативным. ^[7]

arr ( id *** g ) >>> первая f == первая f >>> arr ( id *** g )              

• Передача функции по конвейеру перед упрощением типа должна быть эквивалентна упрощению типа перед подключением к непереданной функции. ^[7]

первый f >>> arr (( s , t ) -> s ) == arr (( s , t ) -> s ) >>> f             

• Наконец, конвейеризация функции дважды перед повторной ассоциацией результирующего кортежа, который является вложенным, должна быть такой же, как повторная ассоциация вложенного кортежа перед присоединением одного обхода функции. Другими словами, сложенные обходы могут быть сглажены путем предварительного объединения вместе тех элементов, которые не были изменены функцией. ^[7]

первый ( первый f ) >>> arr ( (( s , t ), u ) -> ( s ,( t , u ) ) == arr ( (( s , t ), u ) -> ( s ,( t , u ) ) >>> первый f                   

Стрелки могут быть расширены для соответствия конкретным ситуациям путем определения дополнительных операций и ограничений. Обычно используемые версии включают стрелки с выбором, которые позволяют вычислению принимать условные решения, и стрелки с обратной связью , которые позволяют шагу принимать свои собственные выходы в качестве входов. Другой набор стрелок, известный как стрелки с применением, редко используется на практике, поскольку они фактически эквивалентны монадам. ^[6]

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

Хотя ни одна программа не требует стрелок, они обобщают большую часть плотной передачи функций , которую в противном случае потребовал бы чистый декларативный код. Они также могут поощрять повторное использование кода , предоставляя общим связям между шагами программы их собственные определения классов. Возможность применения к типам в общем виде также способствует повторному использованию и сохраняет интерфейсы простыми. ^[6]

Стрелки имеют некоторые недостатки, включая начальные усилия по определению стрелки, которая удовлетворяет законам стрелок. Поскольку монады обычно проще реализовать, а дополнительные возможности стрелок могут быть ненужными, часто предпочтительнее использовать монаду. ^[6] Другая проблема, которая касается многих конструкций функционального программирования , заключается в эффективной компиляции кода со стрелками в императивный стиль, используемый наборами компьютерных инструкций . ^{[ требуется цитата ]}

Из-за необходимости определения arrфункции для подъема чистых функций применимость стрелок ограничена. Например, двунаправленные преобразования не могут быть стрелками, поскольку при использовании нужно было бы предоставить не только чистую функцию, но и ее обратную arr. ^[8] Это также ограничивает использование стрелок для описания реактивных фреймворков на основе push, которые останавливают ненужное распространение. Аналогично, использование пар для объединения значений кортежа приводит к сложному стилю кодирования, который требует дополнительных комбинаторов для перегруппировки значений и поднимает фундаментальные вопросы об эквивалентности стрелок, сгруппированных разными способами. Эти ограничения остаются открытой проблемой, и такие расширения, как Generalized Arrows ^[8] и N-ary FRP ^[9], исследуют эти проблемы.

Большая часть полезности стрелок относится к более общим классам, таким как Profunctor (который требует только пред- и посткомпозиции с функциями), которые имеют применение в оптике. Стрелка по сути является сильным профунктором, который также является категорией, хотя законы немного отличаются.

В Wikibook Haskell есть страница на тему: Стрелки

• Стрелки: общий интерфейс для вычислений
• Новая нотация для стрелок, Росс Патерсон, в ICFP, сентябрь 2001 г.
• Стрелочная нотация ghc руководство