在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键入规则）。