为啥 Münster 编译器认为跨 ++ 的模式匹配是不确定的？

Posted 2023-02-16

【中文标题】为啥 Münster 编译器认为跨 ++ 的模式匹配是不确定的？

【英文标题】：Why does the Münster compiler believe a pattern match across ++ is non-deterministic?为什么 Münster 编译器认为跨 ++ 的模式匹配是不确定的？

【发布时间】：2018-04-04 03:04:47

【问题描述】：

我最近安装了 Münster Curry 编译器来替换我正在使用的速度慢得多的 PAKCS。我想测试的第一件事是我是否可以使用 PAKCS 的一些模式匹配功能，因为我知道一些实现（想到的就是 Sloth）不支持 PAKCS 允许的所有模式匹配。于是我写了如下程序：

import IO

f (a ++ [b]) = a

main = print $ f $ "Hello, World!"

这适用于 PAKCS 并按预期打印 Hello, World，但使用 MCC 编译时出现错误：

Error: cannot duplicate the world

我的理解是，这意味着 MCC 无法跨 ++ 进行模式匹配，但我不明白 MCC 为何选择此错误。 cannot duplicate the world 通常意味着 IO 依赖于非确定性行为。这让我怀疑 MCC 认为我的函数 f 是不确定的。但是据我所知f 是完全确定的。

MCC 做了什么导致它认为我的函数是不确定的？

我不需要知道如何修复程序，这真的很容易，以下工作：

import IO

f (a : b @ (_:_)) = a : f b
f [a] = []

main = print $ f $ "Hello, World!"

我有兴趣了解编译器在此处执行的操作导致其出错，以及这与 PAKCS 在编译代码时执行的操作有何不同。

【参考方案1】：

关于 MCC，我不确定，但 PAKCS 将功能模式转换为（高度）非确定性的表达式。观察到的行为归结为在 IO 中使用非确定性计算时 MCC 和 PAKCS 的不同行为。在 PAKCS 中，计算的是非确定性计算，并且仅当表达式计算为多个结果时才会发生运行时错误。

也就是说，您可以在 PAKCS 中执行以下操作而不会出现运行时错误。

REPL> putStrLn ("Hello" ? failed)
"Hello"

但是，以下计算将产生（相当晚的）运行时错误。

REPL> putStrLn ("Hello" ? "Hello")
Hello
Hello
ERROR: non-determinism in I/O actions occurred!

我猜 MCC 会针对非确定性计算进行不同的（并且更合理；））检查。

最后的一些广告：我通常与KiCS2 合作——您使用 MCC 是否有特定原因？

编辑：如果您想了解更多关于函数式模式及其实现的信息，您可能应该看看以下论文。

Declarative Programming with Function Patterns

【讨论】：

感谢您的回复！这有助于澄清一些事情。至于使用 MCC，我一直想使用 KiCS2，我只是在编译它时遇到了一些问题，所以我想我会尝试 MCC。

如果您对为什么使用函数模式的定义是不确定的更感兴趣，我添加了一篇解释 PAKCS 实现的论文。

关于您在 KiCS2 中遇到的问题：请随时与我联系； )