Система эффектов

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

Система эффектов расширяет понятие типа, включив в него компонент «эффект», который включает в себя вид эффекта и область . Вид эффекта описывает, что делается, а регион описывает, с какими (параметрами) это делается.

Система эффектов обычно является расширением системы типов . термин « система типа и эффекта В этом случае иногда используется ». Часто тип значения вместе с его эффектом обозначается как type ! effect , где и компонент типа, и компонент эффекта упоминают определенные области (например, тип изменяемой ячейки памяти параметризуется меткой области памяти, в которой находится ячейка). Термин «алгебраический эффект» вытекает из системы типов.

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

Примеры

Некоторые примеры поведения, которое можно описать с помощью систем эффектов, включают:

Чтение, запись или выделение памяти: тип эффекта — чтение , запись , выделение или освобождение , а область — это точка программы, в которой было выполнено выделение (т. е. каждой точке программы, где выполняется выделение, присваивается уникальная метка, а область информация статически распространяется по потоку данных). Большинство функций, работающих с памятью, на самом деле будут полиморфными по переменной региона: например, функция, меняющая местами два места в памяти, будет иметь тип forall r1 r2, unit ! {read r1, read r2, write r1, write r2}.
Работа с ресурсами, такими как файлы: например, вид эффекта может быть open , read и close , и опять же, регион — это точка программы, где открывается ресурс.
Передача управления с продолжениями и длинными переходами: тип эффекта может быть goto (т. е. фрагмент кода может выполнять переход) и Comefrom (т. е. фрагмент кода может быть целью перехода), а регион обозначает точку программа, из которой или в которую может быть выполнен переход.

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

Реализации

Основная особенность

Koka — это статически типизированный функциональный язык программирования с алгебраическими обработчиками эффектов в качестве основной функции. ^{[ 3 ]}
Eff — это статически типизированный функциональный язык программирования, основанный на алгебраических обработчиках эффектов. ^{[ 4 ]}
Unison — это статически типизированный функциональный язык программирования с обработчиками алгебраических эффектов (называемыми в языке «способностями») в качестве основной части системы типов. ^{[ 5 ]}
Effekt — это исследовательский язык, основанный на обработчиках эффектов и полиморфных эффектах. ^{[ 6 ]}

Полная поддержка

Haskell — это статически типизированный функциональный язык программирования с несколькими пакетами, позволяющими кодировать эффекты. ^{[ 7 ]} Однако Haskell, как правило, больше ориентирован на монады .
В OCaml 5.0 появилась поддержка экспериментальных примитивов обработчиков эффектов. ^{[ 8 ]} с планами по внедрению правильного синтаксиса высокого уровня в будущем.

Частичная поддержка и прототипы

Scala 3.1 — статически типизированный, функциональный и объектно-ориентированный язык программирования с экспериментальной поддержкой эффектов, ограниченной исключениями , в форме CanThrow возможности. ^{[ 9 ]}
Java — статически типизированный объектно-ориентированный язык программирования; его проверенные исключения представляют собой относительно ограниченный пример системы эффектов. Только один вид эффекта — throws — доступны, нет возможности возобновить работу со значением, и их нельзя использовать с функциями (только методами), если функция не реализует собственный @FunctionalInterface. ^{[ 10 ]}
JavaScript — динамически типизированный язык, в нем есть предложение, реализующее алгебраические эффекты. ^{[ 11 ]}

Ссылки

^ Альбин., Турбак, Франклин (2010). Концепции проектирования на языках программирования . Обучение PHI. ISBN 978-81-203-3996-5 . OCLC 1261053520 . {{cite book}}: CS1 maint: несколько имен: список авторов ( ссылка )
^ Абрамов, Дэн. «Алгебраические эффекты для всех нас» . слишком остро отреагировал.io .
^ «Руководство Кока» . koka-lang.github.io .
^ Претнар, Матия (07 декабря 2021 г.), Eff , получено 11 декабря 2021 г.
^ «Язык Унисона» . www.unisonweb.org . Проверено 7 декабря 2021 г.
^ Исследовательская группа «Эффект». «Язык эффектов: понятия и особенности» . Эффект Языка . Проверено 13 июня 2023 г.
^ Вера, Джош (18 апреля 2020 г.). "joshvera/freemonad-benchmark" . Гитхаб . Тест, сравнивающий производительность различных реализаций свободных монад.
^ «OCaml — Расширения языка» . v2.ocaml.org . Проверено 13 июня 2023 г.
^ «Могу бросать способности» . Документация Скала . Проверено 7 декабря 2021 г.
^ «Функция Lambda Java 8, которая выдает исключение?» . Переполнение стека . Проверено 25 декабря 2021 г.
^ Макавей, Бруно (16 сентября 2020 г.). "macabeus/js-proposal-algebraic-effects: 📐Пусть в JS будут алгебраические эффекты" . Гитхаб .

Главы учебника

Хэнкин, Крис; Нильсон, Флемминг; Нильсон, Ханне Риис (1999). Принципы анализа программ . Берлин: Шпрингер. ISBN 978-3-540-65410-0 .
Гиффорд, Дэвид; Турбак, Франклин А.; Шелдон, Марк А. (2008). «16». Концепции проектирования в языках программирования . Кембридж, Массачусетс: MIT Press. ISBN 978-0-262-20175-9 .

Обзорные документы

Нильсон, Флемминг; Нильсон, Ханне Риис (1999). «Системы типов и эффектов» . Правильный дизайн системы: последние идеи и достижения . Конспекты лекций по информатике . 1710 . Спрингер-Верлаг: 114–136 . дои : 10.1007/3-540-48092-7_6 . ISBN 978-3-540-66624-0 .

Дальнейшее чтение

Марино, Дэниел; Миллштейн, Тодд (2009). «Общая система типов и эффектов». Материалы 4-го международного семинара «Типы в языковом проектировании и реализации» (PDF) . АКМ . п. 39. CiteSeerX 10.1.1.157.8373 . дои : 10.1145/1481861.1481868 . ISBN 9781605584201 . S2CID 14538045 .
Лукассен, Джон М.; Гиффорд, Дэвид К. (1988). «Системы полиморфного эффекта». Материалы 15-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования - POPL '88 . АКМ . стр. 47–57. CiteSeerX 10.1.1.73.4916 . дои : 10.1145/73560.73564 . ISBN 978-0897912525 . S2CID 13015611 .

[1] Альбин., Турбак, Франклин (2010). Концепции проектирования на языках программирования . Обучение PHI. ISBN 978-81-203-3996-5 . OCLC 1261053520 . {{cite book}}: CS1 maint: несколько имен: список авторов ( ссылка )

[2] Абрамов, Дэн. «Алгебраические эффекты для всех нас» . слишком остро отреагировал.io .

[3] «Руководство Кока» . koka-lang.github.io .

[4] Претнар, Матия (07 декабря 2021 г.), Eff , получено 11 декабря 2021 г.

[5] «Язык Унисона» . www.unisonweb.org . Проверено 7 декабря 2021 г.

[6] Исследовательская группа «Эффект». «Язык эффектов: понятия и особенности» . Эффект Языка . Проверено 13 июня 2023 г.

[7] Вера, Джош (18 апреля 2020 г.). "joshvera/freemonad-benchmark" . Гитхаб . Тест, сравнивающий производительность различных реализаций свободных монад.

[8] «OCaml — Расширения языка» . v2.ocaml.org . Проверено 13 июня 2023 г.

[9] «Могу бросать способности» . Документация Скала . Проверено 7 декабря 2021 г.

[10] «Функция Lambda Java 8, которая выдает исключение?» . Переполнение стека . Проверено 25 декабря 2021 г.

[11] Макавей, Бруно (16 сентября 2020 г.). "macabeus/js-proposal-algebraic-effects: 📐Пусть в JS будут алгебраические эффекты" . Гитхаб .

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]