使用递归方案的算法W

Question

我希望能够运用不动点数据类型和递归模式来表述Hindley-Milner类型推断算法。除了递归部分外，忽略所有细节：

w env term = case term of 
    Lam n e -> lam (w (modify1 env) e)
    App a b -> app (w (modify2 env) a) (w (modify3 env) b)
    ...

算法在递归遍历树时构建了一个名为env的环境数据结构，直到达到叶子节点。之后，它在构建结果时使用此信息。

如果没有env部分，则可以简单地使用cata实现。在使用递归方案时，是否可以一般性地实现这一点（使用env）？

- user47376

---

是的，只需将 cata 的目标设置为一个函数 Env -> a。 - luqui

是的，但您可能需要使用具有高阶载体类型的cata，计算可以修改环境并可能失败的操作。 - pigworker

明白了。天才。谢谢。 - user47376

@user47376，它的某些方面感觉有点神奇，不是吗？ - luqui

Answer 1

没有 env 部分，这可以很容易地使用 cata 实现。有了 env，使用递归方案通常可以完成吗？

你要找的是 chronomorphism。它允许你使用未来和过去的 两个 结果进行递归。它并不像听起来那么用户友好，但这是使用递归方案的规范方式。

- user8174234

Answer 2

是的，只需将的目标设置为Env -> a函数。

– luqui

是的，但您可能需要使用更高级承载类型的，计算可以修改环境并可能失败的操作。

– pigworker

- dfeuer

---

现在，使用与拉链和统一变量环境相同的数据结构，将算法W编写为尾递归遍历。你会很高兴做到这一点的。 - pigworker