Тип уникальности
| Типовые системы |
|---|
| Общие понятия |
| Основные категории |
| Второстепенные категории |
В вычислениях уникальный тип гарантирует, что объект используется однопоточным способом и имеет не более одной ссылки на него. Если значение имеет уникальный тип, примененную к нему функцию можно оптимизировать для обновления значения на месте в объектном коде . Такие обновления на месте повышают эффективность функциональных языков , сохраняя при этом ссылочную прозрачность . Уникальные типы также можно использовать для интеграции функционального и императивного программирования.
Введение [ править ]
Типизацию уникальности лучше всего объяснить на примере. Рассмотрим функцию readLine который читает следующую строку текста из данного файла:
function readLine(File f) returns String
return line where
String line = doImperativeReadLineSystemCall(f)
end
end
Сейчас doImperativeReadLineSystemCall считывает следующую строку из файла, используя ОС уровня системный вызов которого является , побочным эффектом изменение текущей позиции в файле. Но это нарушает ссылочную прозрачность, поскольку вызов этого метода несколько раз с одним и тем же аргументом каждый раз будет возвращать разные результаты при перемещении текущей позиции в файле. Это, в свою очередь, делает readLine нарушать ссылочную прозрачность, поскольку он вызывает doImperativeReadLineSystemCall.
Однако, используя типизацию уникальности, мы можем создать новую версию readLine это ссылочно прозрачно, даже если оно построено на основе функции, которая не является ссылочно прозрачной:
function readLine2(unique File f) returns (unique File, String)
return (differentF, line) where
String line = doImperativeReadLineSystemCall(f)
File differentF = newFileFromExistingFile(f)
end
end
The unique декларация указывает, что тип f является уникальным; то есть сказать, что f никогда больше не может быть упомянут вызывающим абонентом readLine2 после readLine2 возвращает, и это ограничение обеспечивается системой типов . И поскольку readLine2 не возвращается f сам по себе, а скорее новый, другой файловый объект differentF, это означает, что это невозможно для readLine2 быть вызванным с f в качестве аргумента, сохраняя тем самым ссылочную прозрачность и допуская возникновение побочных эффектов.
Языки программирования [ править ]
Типы уникальности реализованы в функциональных языках программирования, таких как Clean , Mercury , SAC и Idris . Иногда они используются для выполнения операций ввода-вывода в функциональных языках вместо монад .
было разработано расширение компилятора Для языка программирования Scala , которое использует аннотации для обеспечения уникальности в контексте передачи сообщений между участниками. [1]
Связь с линейной типизацией [ править ]
Уникальный тип очень похож на линейный тип нелинейное значение до такой степени, что эти термины часто используются как взаимозаменяемые, но на самом деле есть различие: фактическая линейная типизация позволяет привести к линейной форме, сохраняя при этом многочисленные ссылки на него. Уникальность гарантирует, что на значение не существует других ссылок, а линейность гарантирует, что на значение больше не может быть сделано никаких ссылок. [2]
Линейность и уникальность можно рассматривать как особенно различные по отношению к модальностям нелинейности и неединственности, но тогда они также могут быть объединены в систему одного типа. [3]
См. также [ править ]
Ссылки [ править ]
- ^ Халлер, П.; Одерский, М. (2010), «Возможности уникальности и заимствования», ECOOP 2010 — Объектно-ориентированное программирование (PDF) , стр. 354–378.
- ^ Уодлер, Филип (17–19 июня 1991 г.). Есть ли польза от линейной логики? . Симпозиум ACM SIGPLAN по частичной оценке и манипулированию программами на основе семантики (PEPM '91). стр. 255–273. CiteSeerX 10.1.1.26.4202 . дои : 10.1145/115865.115894 . ISBN 0-89791-433-3 .
- ^ Маршалл, Дэниел; Воллмер, Майкл; Орчард, Доминик (7 апреля 2022 г.). Линейность и уникальность: сердечное согласие . ESOP'22. дои : 10.1007/978-3-030-99336-8_13 .