在idris中,有一个名为UniqueType
的宇宙,其中类型的值只能使用一次。据我所知,它可以用来编写高性能代码。
但一个值只能使用一次的事实通常太过有限,因此有一种方法可以借用一个值而不是消耗它:
data Borrowed : UniqueType -> BorrowedType where ...
Borrowed
数据类型在 Idris 中的定义如上。为什么它不简单地返回 Type
而是引入另一个类型域 (BorrowedType
)?
最佳答案
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 theRead
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
>/阅读
输入规则)。
关于idris - Idris 的 `BorrowedType` 背后的意图是什么?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/39819709/