linear-types - F* 是否支持线性类型？

Question

根据关于子结构类型系统的维基百科文章，F* 支持某种线性类型。这是真的？如果是这样，怎么做？我在 F* 教程中找不到任何有关它的信息。

Answer 1

F* 的早期版本具有仿射类型（与线性类型密切相关），如 2011 年的本文所述：https ://www.microsoft.com/en-us/research/publication/secure-distributed-programming-with-值依赖类型/

然而，自 2015 年以来的 F* 版本放弃了仿射类型，转而支持其他构造，尤其是一元效应，以对有状态资源进行建模。