говорится больше об уникальности ссылки на объект данного типа

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

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

Код:

function readLine(File f) returns String
      return line where
          String line = doImperativeReadLineSystemCall(f)
      end
  end

Теперь doImperativeReadLineSystemCall считывает следующую строку из файла с использованием системного вызова на уровне ОС, который имеет побочный эффект из-за изменения текущей позиции в файле. Но это нарушает ссылочную прозрачность, потому что вызов этой функции несколько раз с одним и тем же аргументом будет всякий раз возвращать разные результаты при перемещении текущей позиции в файле. Это, в свою очередь, делает readLine нарушающей ссылочную прозрачность, потому что она вызывает callImperativeReadLineSystemCall.
Однако, используя типы с гарантией уникальности, мы можем построить новую версию 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 снова, тем самым сохраняя ссылочную прозрачность и допуская возникновение побочных эффектов.

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

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

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