确定总的终止函数答案

【问题标题】：Determining a total, terminating function确定总的终止函数
【发布时间】：2019-08-09 19:02:50
【问题描述】：

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

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

【问题讨论】：

一种方法，它可能不是你想要的，但它是我会做的，是给出一个满足它的函数的例子。在这种情况下，我有一种感觉，只有一个这样的函数存在（当然可以用几种不同的方式编写，但可能只有一种行为可以满足它）。这是学校作业吗？
不，这只是一个家庭作业问题。但我不确定该怎么做，所以我正在寻找一些指导。
这是一个函数，它接受一个延续，然后通过返回延续结束的初始值来忽略它。
实际上我开始相信这种类型签名没有完全的终止功能。但我不知道我将如何证明这一点，除非有一些非正式的漫谈。如果我给你我的非正式漫谈，我可能会毁了你的任务
...然而，它实际上只有当 c 类型是无约束多态时才等效，这里的参数实际上并非如此——如果类型是 (∀ c . (a -> c) -> c) -> a，这与您给出的不同（并且有可能的实现）。

标签： haskell functional-programming

【解决方案1】：

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

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

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

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

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

【讨论】：

您能否详细说明如何为函数提供参数 if (a :: Void)？（我是否理解正确，这就是你的意思？）
既然你说这个功能不能实现，那是不是只看类型本身就可以判断呢？由于函数的输入是 ((a -> c) -> c) 并且函数应该返回 'a'，因此函数似乎没有办法是总的，因为输入参数是一个函数总是会返回一个'c'？这是看待问题的正确方法吗？
@dvaergiller 我不会在这里展示这个，因为它是家庭作业，OP 应该这样做。
@ceno980 也许你的想法是正确的，但这不是我会接受的家庭作业的解释。