问题标签 [linear-types]

是否有一种合理的方式来表达 .Net（Compact Framework/desktop 3.5 通用子集）中的线性类型的概念，使得 (a) 所需的语法不会变得过于冗长、复杂或其他痛苦和(b) 不变量既可以在运行时强制执行，也可以在编译时通过代码分析进行验证（所以一心一意的维护程序员不能随便忽略不变量）？这里的想法是避免在子系统边界处对命令对象进行防御性复制的需要。

Rust有一个线性类型系统。有什么（好的）方法可以在 OCaml 中模拟这个吗？例如，当使用 ocaml-lua 时，我想确保仅当 Lua 处于特定状态（堆栈顶部的表等）时才调用某些函数。

编辑：这是最近一篇关于与该问题相关的资源多态性的论文：https ://arxiv.org/abs/1803.02796

编辑 2：还有许多关于 OCaml 中会话类型的文章，包括提供一些语法糖的语法扩展。

一个论坛帖子指出使用唯一性类型而不是 STM。我不明白它在说什么。例如，唯一性类型如何处理 STM 试图处理的多个线程正在更新同一变量的问题？

我查看了维基百科关于唯一性类型和线性类型的文章，但仍然不清楚论坛帖子的含义。

So Hacklang is out with a new, fancy type system, where a nullable variable has to be checked before it can be used. What I wonder is, can you achieve something like linear types, statically forcing an order of function calls, the common example being open a file before reading it? In pseudo-code:

Now, $file_handler->read() without open() would rather than throwing a runtime exception, just not compile:

Doable?

(OK, maybe bad example for PHP/Hacklang, since it is not this lowlevel, but you get the idea.)

我正在建模一个系统，该系统具有创建资源的操作和消耗该资源的其他操作。但是，给定的资源只能使用一次 - 有没有办法可以保证在编译时？

具体来说，假设第一个操作烤蛋糕，还有另外两个操作，一个是“选择吃”蛋糕，一个是“选择吃蛋糕”，我只能做一个或另一个。

通过在我们使用蛋糕后在蛋糕上设置一个标志，很容易在运行时强制执行不保留已经吃过的蛋糕（反之亦然）的限制。但是有没有办法在编译时强制执行呢？

顺便说一句，这个问题是为了证明概念，所以我可以接受任何可以给我想要的静态安全的黑魔法。

在仿射类型系统中，资源最多只能使用一次。

从 Hindley-Milner 类型系统开始，似乎一个简单的方法来强制关联是在使用变量的类型规则时从当前类型上下文中简单地删除一个变量（正如LinearML 上的这些幻灯片所建议的，第 15 页）。

这就是执行亲和力的全部内容吗？还是有什么更复杂的事情要做？

在 idris 中，有一个称为类型值的宇宙UniqueType，其中只能使用一次。据我所知，它可以用来编写高性能代码。但是一个值只能使用一次的事实通常太有限了，所以有一种方法可以借用一个值而不是消费它：

数据类型在BorrowedIdris 中定义如上。为什么它不简单地返回Type而是引入另一个类型的宇宙（BorrowedType）？

我最近在 Tweag.IO 上阅读了关于线性类型是一种有用的工具，用于表达仅（确切地）使用一次的参数。他们提供了以下示例：

现在，也许我误解了这个想法，但为什么不能通过以下方式规避：

文章特别提到了论点。这是否也扩展到函数中的所有绑定？

我正在对线性类型进行一些研究，并在 HN 上看到了这个评论。具体来说，它说在

（清洁、ATS 等），线性类型用于编码副作用，作为 monad 的替代方案。

这是什么意思？线性类型如何替代 monad？

此代码按预期编译和工作：

where至少确保只读副本不被保存并且可能在strptr_free.

当然，如果类型系统强制执行它会更好。我的第一次尝试希望它会：

但在字符串模式匹配时失败error(3): the string pattern is ill-typed.

没有铸造就没有办法做到这一点吗？如果没有，我怎样才能在不失去安全性的情况下施放？