UniqueTypeidris には、一度しか使用できない型の値と呼ばれる宇宙があります。私の知る限り、高性能コードの記述に使用できます。しかし、値が 1 回しか使用できないという事実は、通常はあまりにも制限されているため、値を消費する代わりに値を借用する方法があります。
data Borrowed : UniqueType -> BorrowedType where ...
Borrowedデータ型は Idris で上記のように定義されています。Type単純に戻らず、型の別の宇宙 ( BorrowedType)を導入するのはなぜですか?
ドキュメントで説明されているように、型指定された値には制限がBorrowedTypeありBorrowedます。
固有値とは異なり、借用値は必要に応じて何度でも参照できます。ただし、借りた値の使用方法には制限があります。結局のところ、図書館の本や近所の芝刈り機と同じように、関数が値を借りる場合、それを受け取ったときとまったく同じ状態で返すことが期待されます!
制限は、
Borrowed型が一致する場合Read、一意の型を持つ の下のパターン変数は、右側でまったく参照できないことです (それら自体が別の関数に貸与されない限り)。
この制限 (およびlendの寛大さ) は、タイプチェッカーの特別な型付け規則によって実装されます。これらのルールには、適用する何かが必要です。そのためBorrowedType、通常のものとは別の種類にする必要がありますType(特別な規則lendやRead入力規則はありません)。