Тип уникальности

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

Введение [ править ]

Типизацию уникальности лучше всего объяснить на примере. Рассмотрим функцию readLine который читает следующую строку текста из данного файла:

функция readLine(File f) возвращает строку
     обратная линия, где
         Строковая строка = doImperativeReadLineSystemCall(f)
     конец
 конец

Сейчас doImperativeReadLineSystemCallсчитывает следующую строку из файла, используя ОС уровня системный вызов которого является , побочным эффектом изменение текущей позиции в файле. Но это нарушает ссылочную прозрачность, поскольку вызов этого метода несколько раз с одним и тем же аргументом каждый раз будет возвращать разные результаты при перемещении текущей позиции в файле. Это, в свою очередь, делает readLine нарушать ссылочную прозрачность, поскольку он вызывает doImperativeReadLineSystemCall.

Однако, используя типизацию уникальности, мы можем создать новую версию readLine это ссылочно прозрачно, даже если оно построено на основе функции, которая не является ссылочно прозрачной:

функция readLine2(уникальный файл f) возвращает (уникальный файл, строку)
     возврат (различныйF, строка), где
         Строковая строка = doImperativeReadLineSystemCall(f)
         Файл DifferentF = newFileFromExistingFile(f)
     конец
 конец

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 .

Внешние ссылки [ править ]

[1] Халлер, П.; Одерский, М. (2010), «Возможности уникальности и заимствования», ECOOP 2010 — Объектно-ориентированное программирование (PDF) , стр. 354–378.

[2] Уодлер, Филип (17–19 июня 1991 г.). Есть ли польза от линейной логики? . Симпозиум ACM SIGPLAN по частичной оценке и манипулированию программами на основе семантики (PEPM '91). стр. 255–273. CiteSeerX 10.1.1.26.4202 . дои : 10.1145/115865.115894 . ISBN 0-89791-433-3 .

[3] Маршалл, Дэниел; Воллмер, Майкл; Орчард, Доминик (7 апреля 2022 г.). Линейность и уникальность: сердечное согласие . ESOP'22. дои : 10.1007/978-3-030-99336-8_13 .

[1]

[2]

[3]