Система эффектов
 | Эта статья включает список общих ссылок , но в ней отсутствуют соответствующие встроенные цитаты . ( Сентябрь 2010 ) |
В вычислительной технике система эффектов — это формальная система , описывающая вычислительные эффекты компьютерных программ, такие как побочные эффекты . Система эффектов может использоваться для проверки возможных эффектов программы во время компиляции .
Система эффектов расширяет понятие типа, чтобы иметь компонент «эффект», который включает вид эффекта и область . Вид эффекта описывает, что делается, а область описывает, с какими (параметрами) это делается.
Система эффектов обычно является расширением системы типов . В этом случае иногда используется термин « система типов и эффектов ». Часто тип значения обозначается вместе с его эффектом как тип ! эффект , где и компонент типа, и компонент эффекта упоминают определенные области (например, тип изменяемой ячейки памяти параметризуется меткой области памяти, в которой находится ячейка). Термин «алгебраический эффект» вытекает из системы типов.
Системы эффектов могут использоваться для доказательства внешней чистоты некоторых внутренне нечистых определений: например, если функция внутренне выделяет и изменяет область памяти, но тип функции не упоминает эту область, то соответствующий эффект может быть стерт из эффекта функции. [1]
Примеры
Вот некоторые примеры поведения, которые можно описать с помощью систем эффектов:
- Чтение, запись или выделение памяти: тип эффекта — read , write , allocate или free , а регион — это точка программы, где было выполнено выделение (т. е. каждой точке программы, где выполняется выделение, назначается уникальная метка, а информация о регионе статически распространяется по потоку данных). Большинство функций, работающих с памятью, фактически будут полиморфными в переменной region : например, функция, которая меняет местами два местоположения в памяти, будет иметь тип
forall r1 r2, unit ! {read r1, read r2, write r1, write r2}. - Работа с ресурсами, такими как файлы: например, тип эффекта может быть открыт , прочитан и закрыт , и опять же, область — это точка программы, где открывается ресурс.
- Передача управления с продолжениями и длинными переходами: тип эффекта может быть goto (т. е. фрагмент кода может выполнить переход) и comefrom (т. е. фрагмент кода может быть целью перехода), а область обозначает точку программы, из которой или в которую может быть выполнен переход.
С точки зрения программиста, эффекты полезны, поскольку они позволяют отделить реализацию ( как ) конкретных действий от спецификации того, какие действия выполнять. Например, эффект ask name может считывать данные с консоли, выводить окно или просто возвращать значение по умолчанию. Поток управления можно описать как смесь yield (в том, что выполнение продолжается) и throw (в том, что необработанный эффект распространяется вниз, пока не будет обработан). [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]
Ссылки
- ^ Albin., Turbak, Franklyn (2010). Концепции дизайна в языках программирования. PHI Learning. ISBN 978-81-203-3996-5. OCLC 1261053520.
{{cite book}}: CS1 maint: несколько имен: список авторов ( ссылка ) - ^ Абрамов, Дэн. «Алгебраические эффекты для всех нас». overreacted.io .
- ^ "Руководство Koka". koka-lang.github.io .
- ↑ Претнар, Матия (07 декабря 2021 г.), Eff , получено 11 декабря 2021 г.
- ^ "Язык Unison". www.unisonweb.org . Получено 2021-12-07 .
- ^ Исследовательская группа Effekt. "Effekt Language: Concepts and Features". Effekt Language . Получено 2023-06-13 .
- ^ Вера, Джош (18 апреля 2020 г.). "joshvera/freemonad-benchmark". GitHub .
Тест производительности различных реализаций свободной монады.
- ^ "OCaml - Расширения языка". v2.ocaml.org . Получено 2023-06-13 .
- ^ "CanThrow Abilities". Документация Scala . Получено 2021-12-07 .
- ^ "Java 8 Lambda-функция, которая выдает исключение?". Stack Overflow . Получено 25.12.2021 .
Главы учебника
- Ханкин, Крис; Нильсон, Флемминг; Нильсон, Ханне Риис (1999). Принципы анализа программ . Берлин: Шпрингер. ISBN 978-3-540-65410-0.
- Гиффорд, Дэвид; Турбак, Франклин А.; Шелдон, Марк А. (2008). "16". Концепции проектирования в языках программирования . Кембридж, Массачусетс: MIT Press. ISBN 978-0-262-20175-9.
Обзорные статьи
- Нильсон, Флемминг; Нильсон, Ханне Риис (1999). «Системы типов и эффектов» . Правильный дизайн систем: последние идеи и достижения . Конспект лекций по информатике . 1710. Springer-Verlag: 114–136. doi :10.1007/3-540-48092-7_6. ISBN 978-3-540-66624-0.
Дальнейшее чтение
- Марино, Дэниел; Миллстайн, Тодд (2009). "Общая система типов и эффектов". Труды 4-го международного семинара по типам в проектировании и реализации языка (PDF) . ACM . стр. 39. CiteSeerX 10.1.1.157.8373 . doi :10.1145/1481861.1481868. ISBN 9781605584201. S2CID 14538045.
- Lucassen, John M.; Gifford, David K. (1988). "Полиморфные системы эффектов". Труды 15-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования - POPL '88. ACM . стр. 47–57. CiteSeerX 10.1.1.73.4916 . doi :10.1145/73560.73564. ISBN 978-0897912525. S2CID 13015611.
