确定总的终止功能

Question

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

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

Answer 1

为了使函数终止，它是否必须返回一个值（例如，不进入无限循环）？

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

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

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

通常，要证明可以实现某种类型的功能，只需实现即可！...如果可以，那就是在这种情况下不能做到的（（扰流板警报）！为了证明这一点，您需要找到一个特定的类型实例，可以通过调用该函数来为其生成不可能的结果。这样的结果通常可以通过与实例的结果类型变量中找到的Void类型，然后再证明你仍然可以产生一个参数的功能，这将导致一个矛盾，因为功能（通过假设它的总的和终止的），将产生type的值Void，这是不可能的。