idris - Idris 的 `BorrowedType` 背后的意图是什么？

Question

在idris中，有一个名为UniqueType的宇宙，其中类型的值只能使用一次。据我所知，它可以用来编写高性能代码。但一个值只能使用一次的事实通常太过有限，因此有一种方法可以借用一个值而不是消耗它:

data Borrowed : UniqueType -> BorrowedType where ...

Borrowed 数据类型在 Idris 中的定义如上。为什么它不简单地返回 Type 而是引入另一个类型域 (BorrowedType)？

Answer 1

As the documentation explains ，对 BorrowedType 类型的 Borrowed 值有限制:

Unlike a unique value, a borrowed value may be referred to as many times as desired. However, there is a restriction on how a borrowed value can be used. After all, much like a library book or your neighbour’s lawnmower, if a function borrows a value it is expected to return it in exactly the condition in which it was received!

The restriction is that when a Borrowed type is matched, any pattern variables under the Read which have a unique type may not be referred to at all on the right hand side (unless they are themselves lent to another function).

此限制(以及借出的宽大处理)是通过类型检查器中的特殊类型规则实现的。这些规则需要应用一些东西，这就是为什么 BorrowedType 必须是一种与常规 Type 不同的类型(对于常规 Type 来说，没有特殊的 lend >/阅读输入规则)。