haskell - 确定总的终止函数

Question

我正在尝试确定是否为以下类型：((a -> c) -> c) -> a可以使用该类型作为函数签名来编写一个总的终止函数？我知道，为了使一个函数完整，必须为其输入的所有可能值定义它。但是，我不确定函数终止究竟意味着什么。对于要终止的函数，它是否必须返回一个值（例如，而不是进入无限循环）？

此外，我可以使用哪些方法来证明可以使用 来编写总的终止函数((a -> c) -> c) -> a？任何见解都值得赞赏。

标签： haskellfunctional-programming

Answer 1

对于要终止的函数，它是否必须返回一个值（例如，而不是进入无限循环）？

是的，就是这个意思。具体来说，这意味着您不应该通过给出如下定义来作弊

uncont :: ((a -> c) -> c) -> a
uncont f = uncont f

...or uncont = uncont, or uncont = undefined，所有这些都意味着您正在生成一个实际上无法评估为有意义结果的底部值。

---

一般来说，为了证明某种类型的功能可以实现......只需实现它！...如果可以，那就是...（剧透警告）在这种情况下你不能！为了证明这一点，您需要找到一个特定的类型实例化，您可以通过调用该函数生成一个不可能的结果。通常可以通过使用 type 实例化 result-type-variable 来找到这样的结果，Void然后证明您仍然可以为函数生成参数，这会导致矛盾，因为函数（假设它是全部并终止）会产生一个 type 的值Void，这是不可能的。