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

Введение

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

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

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

Примечания