Тип, гарантирующий уникальность

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

Введение

Типы с гарантией уникальности лучше всего объяснить с помощью примера. Рассмотрим функцию 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

Объявление unique указывает, что объект f имеет тип, гарантирующий уникальность; то есть f никогда не может ссылаться на вызывающую функцию readLine2 после возвращения из readLine2, и это ограничение применяется системой типов. И поскольку readLine2 не возвращает f сам, а представляет собой новый, другой файловый объект differentF, это означает, что readLine2 не может быть снова вызвана с аргументом f. Тем самым сохраняется ссылочная прозрачность и допускается возникновение побочных эффектов.

В чистом языке программирования нет изменяемых переменных, а есть только именуемые неизменные значения. Если x имеет гарантированную уникальность, то при вычислении

 x' = f(x)

компилятор гарантирует, что на х больше нигде нет ссылок. Значит в этом месте х использован последний раз, занимаемую им память можно после вычисления f(x) освободить. Если x' и x имеют один тип и размер, то вместо объявления х мусором и выделения памяти для x' можно разместить x' там, где ранее был x. Таким образом получается изменение по месту без нарушения чистоты.

Языки программирования

Типы, гарантирующие уникальность, реализованы в языках функционального программирования Clean, Mercury и Idris. Иногда они используются для выполнения операций ввода-вывода в функциональных языках вместо монад.

Было разработано расширение компилятора для языка программирования Scala, который использует аннотации для обработки уникальности в контексте передачи сообщений между объектами.

Связь с линейной типизацией

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