haskell - 反转折叠

Question

假设我们认为以下是一个好主意:

data Fold x y = Fold {start :: y, step :: x -> y -> y}

fold :: Fold x y -> [x] -> y

在该方案下， length等功能或 sum可以通过调用 fold来实现使用适当的 Fold对象作为论据。

现在，假设您想做一些巧妙的优化技巧。特别是，假设你想写

unFold :: ([x] -> y) -> Fold x y

统治 RULES 应该相对容易。 pragma 使得 fold . unFold = id .但有趣的问题是……我们真的可以实现 unFold吗？ ?

显然你可以使用 RULES应用任意代码转换，无论它们是否保留代码的原始含义。但是你真的能写一个 unFold吗？实际执行其类型签名所暗示的实现？

Answer 1

不，这是不可能的。证明:让

f :: [()] -> Bool
f[] = False
f[()] = False
f _ = True

首先我们必须，对于 f' = unFold f , 有 start f' = False ，因为当折叠空列表时，我们直接得到起始值。那么我们必须要求 step f' () False = False实现 fold f' [()] = False .但是当现在评估 fold f' [(),()] ，我们只会接到一个电话 step f' () False ，我们必须将其定义为 False , 导致 fold f' [(),()] ≡ False , 而 f[(),()] ≡ True .所以不存在 unFold f满足 fold $ unFold f ≡ f . □