问题标签 [st-monad]

这个最近的SO 问题促使我在 Haskell 中编写了一个不安全且纯粹的 ST monad 仿真，您可以在下面看到一个稍微修改过的版本：

如果我们可以在没有unsafeCoerce. 具体来说，我想正式说明通常的 GHC ST monad 和上述仿真起作用的原因。在我看来，它们之所以起作用，是因为：

• 任何STRef s a带有正确s标签的都必须在当前 ST 计算中创建，因为runST确保不会混淆不同的状态。
• 前一点加上 ST 计算只能扩展引用环境这一事实意味着任何STRef s a具有正确s标记的对象都引用了环境中的有效a类型位置（在运行时可能会削弱引用之后）。

以上几点可实现显着的无证明义务的编程体验。在我能想到的安全和纯粹的 Haskell 中，没有什么能比得上真正的；我们可以用索引状态单子和异构列表做一个相当糟糕的模仿，但这并没有表达上述任何一点，因此需要在STRef-s 的每个使用站点进行证明。

我不知道我们如何在 Agda 中正确地将其正式化。对于初学者来说，“在这个计算中分配”已经够棘手了。我曾考虑将STRef-s 表示为特定分配包含在特定ST计算中的证明，但这似乎导致类型索引的无休止递归。

我一直在尝试编写该函数的实现：

但是我每次都因错误而失败：

我现在怀疑实现这个功能是不可能的。

任何人都可以谈论这个吗？我真的很喜欢它的工作，但如果我不能，那么我需要放弃使用Data.Array.ST来编写我的管道。

如何编写以下函数tt，该函数当前存在类型错误：

我认为在里面runST，tt状态变量s可以线程化到函数f中，但是下面的编译器错误告诉我我错了：

任何意见将不胜感激。

我正在尝试构建一个递归函数，为简单起见，假设它需要一个列表并构建一个数组和一个列表。因为我需要在构建数组时读取和写入数组，所以我使用了一个可变数组，所以我可以进行恒定时间的读取和写入。所以签名和函数如下所示：

我想要一个h具有以下签名的函数：

我希望它具有大致以下实现：

问题是，我需要一个g带有这个签名的函数：

但我似乎无法一起破解runST并runSTArray实现这一目标。

无论如何要实施g，还是我应该f首先制作完全不同的签名？

我刚刚发布了这段代码：

我的理由是unsafeThaw在这里使用它是安全的，因为我只indexed解冻xs. 然而，后来我突然想到，元组的未装箱向量——就像这里的这些索引值对——实际上存储为两个未装箱的向量，一个用于索引，一个用于值。indexed因此，实际上根本不会生成新的值向量，而只是将它与索引向量结合起来，这似乎是合理的。在这种情况下，ST-modifyingxsi可能会搞砸xs。

经测试，这似乎并没有发生。我可以依靠这个，还是应该更好地使用thaw？

我最近开始在 Hackage 上查看核心库，并且有一个反复出现的习惯用法我不明白。这是ST 模块的示例：

特别不明白(# new_s, r #)。我假设第二个哈希是指未装箱的值，但其余的对我来说是个谜（大概与“新状态”有关）。

ST monad最初由Launchbury 和 Peyton Jones设计，允许 Haskell 程序员编写命令式代码（使用可变变量、数组等），同时获得该代码的纯接口。

更具体地说，入口点函数的多态类型

确保包含计算的所有副作用ST，并且结果值是纯的。

这曾经被严格（甚至正式）证明过吗？

在编写具有本地类型推断功能的编程语言时（即，它能够推断除函数参数之外的类型，如 Scala），我遇到了循环依赖的问题。

我通过递归探索 AST 来执行类型检查/推理，并将每个可选类型节点延迟映射到类型检查节点。因为任何节点的类型可能取决于 AST 中其他节点的类型，所以我已经打好结这样我可以在推断/检查当前节点的类型时参考其他节点的类型（我保留键入的-AST 在 Reader monad 的环境中）。

这在典型情况下工作得很好，但会因循环依赖而崩溃，因为程序无休止地跟随循环寻找已知类型。

这类问题的解决方案一般（据我所知）是维护一个探索节点的集合，但我想不出在打结时这样做的参照透明方式，因为我事先不知道节点将被访问/评估的顺序，因为这取决于它们彼此之间的依赖关系图。

因此，我似乎需要维护一个本地的、可变的已探索节点集合。为此，我尝试了以下方法：

• 使用 State monad 失败了，因为似乎每个子计算都收到了自己的状态副本，因此无法在计算的不同分支之间共享有关已探索节点的信息。
• 将 IO monad 与 IORefs 一起使用，由于其严格性，这使我无法结缘。
• 与 IORefs 一起使用unsafePerformIO，这引入了突变发生无序或根本不发生的问题。
• 将 ST monad 与 STRefs 一起使用，这引入了与 IO monad 相同的严格问题。

最后，我想出了一个使用 ST monad 的解决方案，在该解决方案中，我在使用 AST 映射时强制进行惰性求值unsafeInterleaveST，这可行，但感觉很脆弱。

是否有更惯用和/或引用透明的解决方案，不是冗长或复杂的？我会包含一个代码示例，但我对这个问题最简单的表述是大约 250 行。

I have written the following code in Haskell using ST monad and it works. My only question is how do I avoid the copy-paste shown in the code below. When I tried to refactor the code, I got compiler errors I could not fully understand. Is there a way to avoid the copy-paste in the code below. I would like to know, if I could refactor the code that processes for start_1 and start_2 (as of now copy/paste) to another helper function.

The error message I get when I try to move the above copy-paste code to a local function (named sieve_factors) created with a 'let' binding is: