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

Question

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

data Borrowed : UniqueType -> BorrowedType where ...

数据类型在BorrowedIdris 中定义如上。为什么它不简单地返回Type而是引入另一个类型的宇宙（BorrowedType）？

Answer 1

正如文档所解释的BorrowedType，对-typedBorrowed值有限制：

与唯一值不同，借用值可以根据需要多次引用。但是，如何使用借入值是有限制的。毕竟，就像图书馆的书或你邻居的割草机一样，如果一个函数借用了一个值，它应该会以它收到时的状态返回它！

限制是当一个Borrowed类型被匹配时，任何Read具有唯一类型的模式变量都不能在右侧被引用（除非它们本身被借给另一个函数）。

此限制（和lend' 的宽大处理）由类型检查器中的特殊类型规则实现。这些规则需要一些东西来应用，这就是为什么BorrowedType必须是一种不同于常规的类型Type（没有特殊lend/Read打字规则）。