Вызов по значению

В языков программирования теории вызов по значению (CBPV) — это промежуточный язык , в который встроены вызова по значению (CBV) и вызова по имени (CBN) стратегии оценки . CBPV структурирован как поляризованное λ-исчисление с двумя основными типами: «значения» (+) и «вычисления» (-). ^[1] Ограничения на взаимодействие между двумя типами обеспечивают контролируемый порядок вычислений, аналогичный монадам или CPS . Исчисление может включать в себя вычислительные эффекты, такие как отсутствие завершения, изменяемое состояние или недетерминизм. Существуют естественные, сохраняющие семантику переводы из CBV и CBN в CBPV. Это означает, что задание семантики CBPV и доказательство ее свойств неявно также устанавливает семантику и свойства CBV и CBN. Пол Блейн Леви сформулировал и развил CBPV в нескольких статьях и своей докторской диссертации. ^[2]^[3]^[4]

Определение

Парадигма CBPV основана на лозунге «ценность есть, а вычисление делает». Одной из сложностей в представлении является различие между переменными типа, зависящими от типов значений, от переменных типов, зависящих от типов вычислений. Эта статья следует за Леви в использовании подчеркиваний для обозначения вычислений, поэтому $B$ является (произвольным) типом значения, но ${\underline {B}}$ — это тип вычислений. ^[4] Некоторые авторы используют другие соглашения, например отдельные наборы букв. ^[5]

Точный набор конструкций зависит от автора и желаемого использования исчисления, но типичны следующие конструкции: ^[2]^[4]

Лямбды λx.M представляют собой вычисления типа $A\to {\underline {B}}$ , где $x:A$ и $M:{\underline {B}}$ . Лямбда-приложение F V или V'F представляет собой вычисление типа ${\underline {B}}$ , где $V:A$ и $F:A\to {\underline {B}}$ . Конструкция let-binding let { x_1 = V_1; ... }. M связывает значения x_1 к ценностям V_1, совпадающих типов $A_{1}$ , внутри вычисления M : ${\underline {B}}$ .
Громкий звук thunk M это значение типа $U{\underline {A}}$ построенный на основе вычислений M типа ${\underline {A}}$ . Принуждение к мысли — это вычисление, force X : ${\underline {A}}$ для размышления X : $U{\underline {A}}$ .
Также возможно обернуть значение V типа $A$ как вычисление return V : $FA$ . Такое вычисление может использоваться внутри другого вычисления как M to x. N : ${\underline {B}}$ , где M : $FA$ , и N : ${\underline {B}}$ это вычисление.
Значения также могут включать в себя алгебраические типы данных, созданные из тега и нуля или более подзначений, а вычисления включают в себя деконструкцию сопоставления с образцом. match V as { (1,...) in M_1, ... }. В зависимости от представления АТД могут быть ограничены двоичными суммами и произведениями, только логическими значениями или вообще отсутствовать.

Программа — это закрытое вычисление типа $FA$ , где $A$ представляет собой наземный тип ADT. ^[4]

Комплексные значения

Такие выражения, как not true : bool иметь смысл денотационно. Но, следуя приведенным выше правилам, not может быть закодировано только с использованием сопоставления с образцом, что делает его вычислением, и поэтому общее выражение также должно быть вычислением, что дает not true : F bool. Аналогично нет возможности получить 1 от (1,2) без построения вычислений. При моделировании CBPV в эквациональной теории или теории категорий такие конструкции незаменимы. Поэтому Леви определяет расширенный IR: «CBPV с комплексными значениями». Этот IR расширяет привязку let для привязки значений в выражении значения, а также для сопоставления значения с шаблоном, когда каждое предложение возвращает выражение значения. ^[3] Помимо моделирования, такие конструкции также делают написание программ на CBPV более естественным. ^[2]

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

Перевод

Трансляция CBV создает значения CBPV для каждого выражения. Функция CBV λx.M : $A\to _{v}B$ переводится на thunk λx.M^v : $U(A^{v}\to FB^{v})$ . Приложение CBV M N : $A$ переводится в вычисление M^v to f in N^v to x in x'(force f) типа $FA$ , делая порядок вычислений явным. Соответствие шаблону match V as { (1,...) in M_1, ... } переводится как V^v to z in match z as { (1,...) in M_1^v, ... }. Значения заключены в return при необходимости, но в остальном остаются неизмененными. ^[2] В некоторых переводах может потребоваться секвенирование, например, при переводе inl M к M to x. return inl x. ^[4]

Трансляция CBN производит вычисления CBPV для каждого выражения. Функция CBN λx.M : $A\to B$ переводится без изменений, λx.M^N : $(UA^{n})\to X^{n}$ . Приложение CBN M N : $C$ переводится в вычисление M^v (thunk N^v) типа $C^{n}$ . Соответствие шаблону match V as { (1,...) in M_1, ... } переводится аналогично CBN как Vⁿ to z in match z as { (1,...) in M_1ⁿ, ... }. Значения ADT заключены в return, но force и thunk также необходимы по внутренней структуре. Перевод Леви предполагает, что M = force (thunk M), что действительно имеет место. ^[2]

Также возможно расширить CBPV до модели «вызов по мере необходимости», введя M need x. N конструкция, которая обеспечивает видимое совместное использование. Эта конструкция имеет семантику, аналогичную M name x. N = (λy.N[x ↦ (force y)])(thunk M), за исключением того, что с need конструкция, мысль о M оценивается не более одного раза. ^[6]

Модификации

Некоторые авторы отмечают, что CBPV можно упростить, удалив либо конструктор типа U (thunks), либо конструктор типа U (thunks). ^[7] или конструктор типа F (вычисления, возвращающие значения). ^[8] Эггер и Могельберг оправдывают исключение U тем, что упрощают синтаксис и позволяют избежать беспорядка, связанного с необъяснимыми преобразованиями вычислений в значения. Этот выбор делает типы вычислений подмножеством типов значений, и тогда естественно расширять типы функций до полного функционального пространства между значениями. Они называют свое исчисление «исчислением расширенных эффектов». Это модифицированное исчисление эквивалентно расширенному набору CBPV посредством двунаправленного перевода, сохраняющего семантику. ^[7] Эрхард, напротив, опускает конструктор типа F, делая значения подмножеством вычислений. Эрхард переименовывает вычисления в «общие типы», чтобы лучше отражать их семантику. Это модифицированное исчисление, «полуполяризованное лямбда-исчисление», тесно связано с линейной логикой. ^[8]^[9] Его можно двунаправленно перевести в подмножество полностью поляризованного варианта CBPV. ^[10]

См. также

Программирование вычислимых функций

Ссылки

^ Каввос, Джорджия; Морхаус, Эдвард; Ликата, Дэниел Р.; Даннер, Норман (январь 2020 г.). «Извлечение повторений для функциональных программ посредством вызова по значению» . Труды ACM по языкам программирования . 4 (ПОПЛ): 1–31. arXiv : 1911.04588 . дои : 10.1145/3371083 . ISSN 2475-1421 .
^ Перейти обратно: ^а ^б ^с ^д ^и Блейн Леви, Пол (апрель 1999 г.). Вызов по значению push: парадигма включения (PDF) . Типизированное лямбда-исчисление и приложения, 4-я Международная конференция, TLCA'99, Л'Акуила, Италия. Конспекты лекций по информатике. Том. 1581. стр. 228–242.
^ Перейти обратно: ^а ^б ^с Леви, Пол Блейн (2003). Вызов по значению: функционально-императивный синтез (PDF) . Дордрехт ; Бостон: Академическое издательство Kluwer. ISBN 978-1-4020-1730-8 .
^ Перейти обратно: ^а ^б ^с ^д ^и ^ж Леви, Пол Блейн (апрель 2022 г.). «Вызов по значению нажатия». Новости ACM SIGLOG . 9 (2): 7–29. дои : 10.1145/3537668.3537670 .
^ Педро, Пьер-Мари; Табаро, Николя (январь 2020 г.). «Огненный треугольник: как сочетать замену, зависимое устранение и эффекты». Труды ACM по языкам программирования . 4 (ПОПЛ): 1–28. дои : 10.1145/3371126 .
^ Макдермотт, Дилан; Майкрофт, Алан (2019). «Расширенный вызов по значению push: рассуждения об эффективных программах и порядке оценки». Языки и системы программирования . Международное издательство Спрингер. стр. 235–262. дои : 10.1007/978-3-030-17184-1_9 . ISBN 978-3-030-17184-1 .
^ Перейти обратно: ^а ^б Эггер, Дж.; Могельберг, RE; Симпсон, А. (1 июня 2014 г.). «Расширенное исчисление эффектов: синтаксис и семантика» (PDF) . Журнал логики и вычислений . 24 (3): 615–654. дои : 10.1093/logcom/exs025 .
^ Перейти обратно: ^а ^б Эрхард, Томас (2016). «Вызов по значению с точки зрения линейной логики». Языки и системы программирования . Конспекты лекций по информатике. Том. 9632. стр. 202–228. дои : 10.1007/978-3-662-49498-1_9 . ISBN 978-3-662-49497-4 .
^ Шуке, Жюль; Тассон, Кристина (2020). Расширение Тейлора для Call-By-Push-Value . Лейбниц Международные труды по информатике. Том 152. Замок Дагштуль - Центр информатики Лейбница. стр. 16:1–16:16. doi : 10.4230/LIPIcs.CSL.2020.16 .
^ Эрхард, Томас (июль 2015 г.), FPC с вызовом по значению и его интерпретация в линейной логике

[Kavvos2020-1] Каввос, Джорджия; Морхаус, Эдвард; Ликата, Дэниел Р.; Даннер, Норман (январь 2020 г.). «Извлечение повторений для функциональных программ посредством вызова по значению» . Труды ACM по языкам программирования . 4 (ПОПЛ): 1–31. arXiv : 1911.04588 . дои : 10.1145/3371083 . ISSN 2475-1421 .

[Levy99-2] Перейти обратно: ^а ^б ^с ^д ^и Блейн Леви, Пол (апрель 1999 г.). Вызов по значению push: парадигма включения (PDF) . Типизированное лямбда-исчисление и приложения, 4-я Международная конференция, TLCA'99, Л'Акуила, Италия. Конспекты лекций по информатике. Том. 1581. стр. 228–242.

[Levy2003-3] Перейти обратно: ^а ^б ^с Леви, Пол Блейн (2003). Вызов по значению: функционально-императивный синтез (PDF) . Дордрехт ; Бостон: Академическое издательство Kluwer. ISBN 978-1-4020-1730-8 .

[Levy2022-4] Перейти обратно: ^а ^б ^с ^д ^и ^ж Леви, Пол Блейн (апрель 2022 г.). «Вызов по значению нажатия». Новости ACM SIGLOG . 9 (2): 7–29. дои : 10.1145/3537668.3537670 .

[5] Педро, Пьер-Мари; Табаро, Николя (январь 2020 г.). «Огненный треугольник: как сочетать замену, зависимое устранение и эффекты». Труды ACM по языкам программирования . 4 (ПОПЛ): 1–28. дои : 10.1145/3371126 .

[6] Макдермотт, Дилан; Майкрофт, Алан (2019). «Расширенный вызов по значению push: рассуждения об эффективных программах и порядке оценки». Языки и системы программирования . Международное издательство Спрингер. стр. 235–262. дои : 10.1007/978-3-030-17184-1_9 . ISBN 978-3-030-17184-1 .

[Egger2014-7] Перейти обратно: ^а ^б Эггер, Дж.; Могельберг, RE; Симпсон, А. (1 июня 2014 г.). «Расширенное исчисление эффектов: синтаксис и семантика» (PDF) . Журнал логики и вычислений . 24 (3): 615–654. дои : 10.1093/logcom/exs025 .

[Ehrhard2016-8] Перейти обратно: ^а ^б Эрхард, Томас (2016). «Вызов по значению с точки зрения линейной логики». Языки и системы программирования . Конспекты лекций по информатике. Том. 9632. стр. 202–228. дои : 10.1007/978-3-662-49498-1_9 . ISBN 978-3-662-49497-4 .

[9] Шуке, Жюль; Тассон, Кристина (2020). Расширение Тейлора для Call-By-Push-Value . Лейбниц Международные труды по информатике. Том 152. Замок Дагштуль - Центр информатики Лейбница. стр. 16:1–16:16. doi : 10.4230/LIPIcs.CSL.2020.16 .

[10] Эрхард, Томас (июль 2015 г.), FPC с вызовом по значению и его интерпретация в линейной логике

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]