В вычислениях уникальный тип гарантирует, что объект используется однопоточным способом , максимум с одной ссылкой на него. Если значение имеет уникальный тип, функция, примененная к нему, может быть оптимизирована для обновления значения на месте в объектном коде . Такие обновления на месте повышают эффективность функциональных языков , сохраняя при этом ссылочную прозрачность . Уникальные типы также могут использоваться для интеграции функционального и императивного программирования.
Типизацию уникальности лучше всего объяснить на примере. Рассмотрим функцию readLine, которая считывает следующую строку текста из заданного файла:
функция readLine(File f) возвращает строку обратная линия где Строка строки = doImperativeReadLineSystemCall(f) конецконецТеперь doImperativeReadLineSystemCallсчитывает следующую строку из файла, используя системный вызов уровня ОС , побочным эффектом которого является изменение текущей позиции в файле. Но это нарушает ссылочную прозрачность, поскольку вызов его несколько раз с тем же аргументом будет возвращать разные результаты каждый раз, поскольку текущая позиция в файле перемещается. Это, в свою очередь, нарушает ссылочную прозрачность, поскольку он вызывает .readLinedoImperativeReadLineSystemCall
Однако, используя типизацию уникальности, мы можем построить новую версию, readLineкоторая будет ссылочно прозрачной, даже если она построена поверх функции, которая ссылочно не прозрачна:
функция readLine2(уникальный Файл f) возвращает (уникальный Файл, Строка) возврат (differentF, строка) где Строка строки = doImperativeReadLineSystemCall(f) Файл другойF = новыйФайлИзСуществующегоФайла(f) конецконецВ uniqueобъявлении указано, что тип fуникален; то есть он fникогда не может быть снова упомянут вызывающим объектом readLine2после readLine2возврата, и это ограничение налагается системой типов . И поскольку readLine2не возвращает fсебя, а возвращает новый, другой файловый объект differentF, это означает, что его невозможно readLine2вызвать fв качестве аргумента когда-либо снова, тем самым сохраняя ссылочную прозрачность, но допуская возникновение побочных эффектов.
Типы уникальности реализованы в функциональных языках программирования, таких как Clean , Mercury , SAC и Idris . Иногда они используются для выполнения операций ввода-вывода в функциональных языках вместо монад .
Для языка программирования Scala было разработано расширение компилятора , которое использует аннотации для обработки уникальности в контексте передачи сообщений между акторами. [1]
Уникальный тип очень похож на линейный тип , до такой степени, что эти термины часто используются взаимозаменяемо, но на самом деле есть различие: фактическая линейная типизация позволяет преобразовать нелинейное значение в линейную форму, сохраняя при этом множественные ссылки на него. Уникальность гарантирует, что значение не имеет других ссылок на него, в то время как линейность гарантирует, что на значение не может быть сделано больше ссылок. [2]
Линейность и уникальность можно рассматривать как особенно различные по отношению к модальностям нелинейности и неуникальной уникальности, но затем их можно объединить в единую систему типов. [3]