haskell - 是否有任何非递归项可以折叠在斯科特编码列表上？

Question

假设我有一个scott 编码的列表，例如：

scott = (\ c n -> c 1 (\ c n -> c 2 (\ c n -> c 3 (\ c n -> n))))

我想要一个接收此类列表并将其转换为实际列表（[1,2,3]）的函数，但此类函数不能递归。也就是说，它必须是 eta-beta 范式。有这个功能吗？

Answer 1

好的，我试一试。请随时纠正我，因为我不是这方面的专家。

对于任意xand xs，它必须是toList (\c n -> c x xs)简化为可转换为 的项的情况x : toList xs。

c x xs这只有在我们通过应用(\c n -> c x xs)一些c和来减少左手边时才有可能n。所以toList ~ (\f -> f ? ?)。（顺便说一句，这是我想不出一个很好的严谨论证的部分；我有一些想法，但没有一个很好。我很乐意听到提示）。

现在一定是这样c x xs ~ (x : toList xs)。但是由于x和xs是不同的全称变量，并且它们是唯一出现在右手边的变量，所以方程属于米勒模式片段，因此c ~ (\x xs -> x : toList xs)是其最一般的解。

所以，toList必须减少到(\f -> f (\x xs -> x : toList xs) n)一些n。显然，toList不能有一个范式，因为我们总是可以展开递归的出现。