Что такое система типов и эффектов?

Question

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

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

Answer 1

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

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

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

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

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

• Типы атомарности:Статическая проверка и вывод для Java.Фланаган, Фрейнд, Липшин и Кадир.
• Обеспечение соблюдения протоколов высокого уровня в программном обеспечении низкого уровня.Роберт ДеЛайн и Мануэль Фендрих.
• Системы типов и эффектов.Нильсон и Нильсон.

Answer 2

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

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

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

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

Answer 3

Вы можете посмотреть http://www.haskell.org/haskellwiki/DDC

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