haskell - 确定总的终止函数

Question

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

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

Answer 1

For a function to be terminating, does it have to return a value (and not go into an infinite loop for example)?

是的，就是这个意思。具体来说，这意味着您不应该通过给出类似的定义来欺骗

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

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

---

通常，为了证明某种类型的函数可以实现......只需实现它即可! ...如果你可以，那就是...(剧透警告)在这种情况下你不能!为了证明这一点，您需要找到一个特定的类型实例，通过调用该函数可以为其生成不可能的结果。通常可以通过使用 the Void type 实例化结果类型变量来找到此类结果。 ，然后证明您仍然可以为该函数生成一个参数，这会导致矛盾，因为该函数(假设它是完整的并终止)将生成一个 Void< 类型的值，这是不可能的。