Что за Идриса «Заимствовано»?

Question

В idris есть вселенная под названием UniqueType значения типов, в которых можно использовать только один раз. Насколько мне известно, его можно использовать для написания высокопроизводительного кода. Но тот факт, что значение может быть использовано только один раз, как правило, слишком ограничены, так что есть способ заимствовать значение вместо того, чтобы потреблять его:

data Borrowed : UniqueType -> BorrowedType where ... 

Тип Borrowed данных определяется, как указано выше в Идриса. Почему он просто не возвращает Type, а вводит другую вселенную типов (BorrowedType)?

Answer 1

As the documentation explains, есть ограничение на BorrowedType -typed Borrowed значения:

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

Ограничение на то, что при сопоставлении типа Borrowed любые переменные шаблона под Read, которые имеют уникальный тип, могут не упоминаться вообще с правой стороны (если только они сами не переданы другой функции).

Это ограничение (и снисходительность lend) реализовано специальными правилами ввода текста в typechecker. Этим правилам нужно что-то применять, поэтому BorrowedType должен быть разного рода, чем обычный Type (для которого нет специальных lend/Read правил ввода).