| Системы типов |
|---|
| Общие понятия |
| Основные категории |
| Второстепенные категории |
| Смотрите также |
В вычислении , а уникальный тип гарантирует , что объект используется в однопоточных образом, с не более одной ссылки на него. Если значение имеет уникальный тип, применяемую к нему функцию можно оптимизировать для обновления значения на месте в объектном коде . Такие обновления на месте повышают эффективность функциональных языков , сохраняя при этом ссылочную прозрачность . Уникальные типы также могут использоваться для интеграции функционального и императивного программирования.
Введение [ править ]
Уникальность набора текста лучше всего пояснить на примере. Рассмотрим функцию, readLineкоторая читает следующую строку текста из заданного файла:
функция readLine ( File f ) возвращает строку возврата String, где String line = doImperativeReadLineSystemCall ( f ) конецконецТеперь doImperativeReadLineSystemCallчитает следующую строку из файла , используя OS -level системный вызов , который имеет побочный эффект изменения текущей позиции в файле. Но это нарушает ссылочную прозрачность, потому что вызов его несколько раз с одним и тем же аргументом будет возвращать разные результаты каждый раз, когда текущая позиция в файле перемещается. Это, в свою очередь, readLineнарушает ссылочную прозрачность, потому что вызывает doImperativeReadLineSystemCall.
Однако, используя типизацию уникальности, мы можем создать новую версию, readLineкоторая будет ссылочно прозрачной, даже если она построена поверх функции, которая не является ссылочно прозрачной:
функция readLine2 ( уникальный файл f ) возвращает ( уникальный файл , строка ) return ( differentF, line ), где String line = doImperativeReadLineSystemCall ( f ) File differentF = newFileFromExistingFile ( f ) конецконецВ uniqueдекларации указывает , что тип fявляется уникальным; это означает, что на него fбольше никогда не может ссылаться вызывающая функция readLine2after readLine2return, и это ограничение обеспечивается системой типов . А поскольку readLine2возвращает не fсам себя, а новый, другой файловый объект differentF, это означает, что его невозможно readLine2вызвать fснова в качестве аргумента, тем самым сохраняя ссылочную прозрачность, позволяя возникать побочные эффекты.
Языки программирования [ править ]
Типы уникальности реализованы в языках функционального программирования, таких как Clean , Mercury , SAC и Idris . Иногда они используются для выполнения операций ввода-вывода на функциональных языках вместо монад .
Для языка программирования Scala было разработано расширение компилятора, которое использует аннотации для обработки уникальности в контексте передачи сообщений между участниками. [1]
Связь с линейной типизацией [ править ]
Уникальный тип очень похож на линейный тип до такой степени, что термины часто используются взаимозаменяемо, но на самом деле есть различие: фактическая линейная типизация позволяет нелинейному значению быть приведенным к линейной форме, при этом сохраняя множественные ссылки на него. Уникальность гарантирует, что у значения нет других ссылок на него, в то время как линейность гарантирует, что на значение больше нельзя ссылаться. [2]
См. Также [ править ]
- Линейный тип
- Линейная логика
Ссылки [ править ]
- ^ Haller, P .; Одерский М. (2010), «Возможности уникальности и заимствования», ECOOP 2010 - объектно-ориентированное программирование (PDF) , стр. 354–378
- ^ Wadler, Филипп (17-19 июня 1991). Есть ли польза от линейной логики? . Симпозиум ACM SIGPLAN по частичному вычислению и управлению программами на основе семантики (PEPM '91). С. 255–273. CiteSeerX 10.1.1.26.4202 . DOI : 10.1145 / 115865.115894 . ISBN 0-89791-433-3.
Внешние ссылки [ править ]
 | Использование внешних ссылок в этой статье может не соответствовать политикам или рекомендациям Википедии . ( Февраль 2013 г. ) ( Узнайте, как и когда удалить этот шаблон сообщения ) |
- Библиография по линейной логике
- Упрощенный ввод уникальности
- Работы Филипа Вадлера по линейной логике
Обсуждение уникальности набора текста в языках программирования [ править ]
- Живой линейный лисп - «Смотри, мама, без мусора!»
- Стеки линейной логики и перестановок - четвертый должен быть первым
- Минимизация обновления счетчика ссылок с помощью отложенных и привязанных указателей для функциональных структур данных
- Одноразовые переменные и линейные объекты - управление хранилищем, отражение и многопоточность
Эксперименты с уникальностью набора текста (с точки зрения производительности) [ править ]
- Быстрая сортировка по "линейной логике"
- Тест Бойера соответствует линейной логике
- Разреженные многочлены и линейная логика
