uniqueness-typing

4熱度

1回答

Idris'`BorrowedType`背後的意圖是什麼？

在idris中，有一個名爲UniqueType的宇宙，其中只能使用一次的類型的值。據我所知，它可以用來編寫高性能的代碼。但這一個值只能使用一次的事實，通常是太有限的，所以有一種方法來借用一個值，而不是消耗它的： data Borrowed : UniqueType -> BorrowedType where ... 的Borrowed數據類型被定義爲上述伊德里斯。它爲什麼不簡單地返回Type