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

Question

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

Answer 1

早期版本的 F* 具有仿射类型(与线性类型密切相关)，如 2011 年的这篇论文所述:https://www.microsoft.com/en-us/research/publication/secure-distributed-programming-with-value-dependent-types/

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