Подтвердить что ты не робот

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

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

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

Ответ 1

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

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

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

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

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

Ответ 2

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

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

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

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