Что такое система типов и эффектов? - PullRequest
14 голосов
/ 13 октября 2008

Статья из Википедии о Система эффектов в настоящее время является просто короткой заглушкой, и я некоторое время задавался вопросом, что такое система эффектов.

  • Существуют ли языки, которые имеют систему эффектов в дополнение к системе типов?
  • На что похожа возможная (гипотетическая) запись в основном потоке , с которым вы знакомы, с эффектами?

Ответы [ 3 ]

17 голосов
/ 13 октября 2008

«Система типов и эффектов» описывает не только виды значений в программе, но и изменения этих значений. Проверка "Typestate" является связанной идеей.

Примером может служить система типов, которая отслеживает дескрипторы файлов: вместо функции close с типом возвращаемого значения void система типов будет записывать эффект из close как удаление файловый ресурс - любая попытка чтения или записи в файл после вызова close станет ошибкой типа.

Мне неизвестно о какой-либо системе типов и эффектов, появляющейся в основном языке программирования. Они использовались для определения статического анализа (например, вполне естественно определить анализ для правильной блокировки / разблокировки с точки зрения эффектов). Таким образом, системы эффектов обычно определяются с использованием схем логического вывода, а не конкретного синтаксиса. Вы можете представить себе синтаксис, похожий на

File open(String name) [+File]; // open creates a new file handle
void close(File f)     [-f]   ; // close destroys f 

Если вы хотите узнать больше, могут быть интересны следующие статьи (справедливое предупреждение: статьи довольно теоретические).

7 голосов
/ 13 октября 2008

(Это не авторитетный ответ; просто пытаюсь тралить мою память.)

В некотором смысле, каждый раз, когда вы кодируете «монаду состояния» на языке, вы используете систему типов в качестве системы потенциальных эффектов. Таким образом, «State» или «IO» в Haskell отражают это понятие (IO также включает в себя множество других эффектов). Я смутно помню, как читал статьи о различных языках, в которых используются усовершенствованные системы типов, в том числе такие вещи, как «зависимые типы», для контроля более детального управления эффектами, так что, например, система типа / эффекта могла собирать информацию о том, какие области памяти будут изменены в данный тип данных. Это полезно, так как предоставляет способы заставить две функции, которые изменяют взаимоисключающие биты состояния, иметь возможность «коммутировать» (монады обычно не коммутируют, а разные монады не всегда хорошо сочетаются друг с другом, что часто делает это трудно набрать (читай: назначить статический тип) «разумным» программам ...

Аналогия на очень волнообразном уровне - это то, как Java проверила исключения. Вы выражаете дополнительную информацию в системе типов об определенных эффектах (вы можете рассматривать исключение как «эффект» для целей аналогии), но эти «эффекты» обычно просачиваются по всей вашей программе и плохо сочетаются в попрактикуйтесь (в итоге вы получите миллион предложений «throws» или прибегнете ко множеству непроверенных типов исключений во время выполнения).

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

4 голосов
/ 04 декабря 2009

Вы можете взглянуть на http://www.haskell.org/haskellwiki/DDC

Это версия Haskell, реализующая систему эффектов.

...