idrisには、UniqueTypeという名前のユニバースがあり、そのタイプの値は1回しか使用できません。私が知る限り、これを使用して高性能コードを書くことができます。 は、しかし、値が一度だけ使用することができるという事実は、通常はあまりにも限られているので、それを消費するのではなく、値を借りする方法があります：Idrisの「BorrowedType」の意図は何ですか？
data Borrowed : UniqueType -> BorrowedType where ...
Borrowedデータ型はイドリスで、上記のように定義されます。なぜそれは単にTypeを返すのではなく、別のタイプの世界（BorrowedType）を紹介していますか？
As the documentation explains、BorrowedType上の制限があるBorrowed値-typed：所望のようにユニークな値、借り値異なり
が何回呼ばれてもよいです。ただし、借用価値の使用方法には制限があります。結局のところ、図書館の本や隣人の芝刈り機のように、関数が値を借りれば、受け取った状態で返すことが期待されます。
Borrowedタイプが一致する場合、ユニークタイプを持つReadの下のパターン変数は、（別の関数に貸し出されていない限り）右側では全く参照されない可能性があります。
この制限（およびlendの寛容）は、型チェッカーの特別な型付け規則によって実装されます。これらのルールには何かが必要です。そのため、BorrowedTypeは通常のTypeとは別の種類でなければなりません（そのためには特別なlend/Readタイピングルールはありません）。