盛安安*_*盛安安 5 linear-types idris uniqueness-typing
在 idris 中，有一个称为UniqueType类型值的宇宙，其中只能使用一次。据我所知，它可以用来编写高性能代码。但是一个值只能使用一次的事实通常太有限了，所以有一种方法可以借用一个值而不是消费它：
data Borrowed : UniqueType -> BorrowedType where ...
该Borrowed数据类型被定义为在以上伊德里斯。为什么它不简单地返回Type而是引入另一个类型的宇宙 ( BorrowedType)？
正如文档所解释的BorrowedType，对-typedBorrowed值有限制：
\n\n与唯一值不同，借用值可以根据需要多次被引用。但是，借用价值的使用方式存在限制。毕竟，就像图书馆的书或你邻居的割草机\xe2\x80\x99s 割草机一样，如果函数借用了一个值，那么它应该以与接收时完全相同的状态返回它！
\n限制是，当
\nBorrowed类型匹配时，其下Read具有唯一类型的任何模式变量可能根本不会在右侧被引用（除非它们本身借给另一个函数）。
这种限制（以及lend\的宽大处理）是通过类型检查器中的特殊类型规则来实现的。这些规则需要应用一些东西，这就是为什么BorrowedType必须是一种与常规规则不同的类型Type（没有特殊lend/Read打字规则）。