在idris中，有一個名爲UniqueType的宇宙，其中只能使用一次的類型的值。據我所知，它可以用來編寫高性能的代碼。 但這一個值只能使用一次的事實，通常是太有限的，所以有一種方法來借用一個值，而不是消耗它的：Idris'`BorrowedType`背後的意圖是什麼？
data Borrowed : UniqueType -> BorrowedType where ...
的Borrowed數據類型被定義爲上述伊德里斯。它爲什麼不簡單地返回Type，而是引入另一個類型的宇宙（BorrowedType）？
As the documentation explains，有限制上BorrowedType -typed Borrowed值：
不像的唯一值，如所期望借來值可以被稱爲多次。但是，如何使用借來的價值是有限制的。畢竟，就像一本圖書館書或你的鄰居的割草機，如果一個函數借用了一個值，那麼它就會按照收到的條件返回它！
的限制是，當一個
Borrowed類型匹配時，下Read任何圖案的變量，其具有獨特的類型可以不被稱爲在所有在右手側（除非它們本身借給另一個功能）。
這個限制（和lend的寬大）是通過typechecker中的特殊輸入規則來實現的。這些規則需要適用的東西，這就是爲什麼BorrowedType必須是一個獨立的類型比普通Type（其中沒有特殊的lend/Read鍵入規則）。