5

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

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规则这样的编译指示应该相对容易fold . unFold = id。但有趣的问题是……我们真的可以实现 unFold吗？

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

4

4 回答 4

12

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

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

首先我们必须， for f' = unFold f， have 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。□</p>

于 2012-10-18T08:34:09.240 回答
7

你可以，但你需要对它进行轻微的修改Fold才能把它拉下来。

列表上的所有函数都可以表示为折叠，但有时为了实现这一点，需要额外的簿记。假设我们向您的类型添加了一个额外的类型参数Fold，它传递了这个额外的上下文信息。

data Fold a c r = Fold { _start :: (c, r), _step :: a -> (c,r) -> (c,r) }

现在我们可以fold像这样实现

fold :: Fold a c r -> [a] -> r
fold (Fold step start) = snd . foldr step start

现在，当我们试图走另一条路时会发生什么？

unFold :: ([a] -> r) -> Fold a c r

从哪里来c？函数是不透明的值，因此很难知道如何检查函数并知道它依赖于哪些上下文信息。所以，让我们作弊一点。我们将“上下文信息”作为整个列表，所以当我们到达最左边的元素时，我们可以将函数应用于原始列表，忽略之前的累积结果。

unFold :: ([a] -> r) -> Fold a [a] r
unFold f = Fold { _start = ([], f [])
                , _step = \a (c, _r) -> let c' = a:c in (c', f c') }

现在，可悲的是，这不一定与 组成fold，因为它要求c必须是[a]。让我们通过c存在量化隐藏来解决这个问题。

{-# LANGUAGE ExistentialQuantification #-}
data Fold a r = forall c. Fold
  { _start :: (c,r)
  , _step :: a -> (c,r) -> (c,r) }

fold :: Fold a r -> [a] -> r
fold (Fold start step) = snd . foldr step start

unFold :: ([a] -> r) -> Fold a r
unFold f = Fold start step where
  start = ([], f [])
  step a (c, _r) = let c' = a:c in (c', f c')

现在，它应该永远是真的fold . unFold = id。并且，给定Fold数据类型相等的宽松概念，您也可以说unFold . fold = id. 您甚至可以提供一个智能构造函数，其作用类似于旧Fold构造函数：

makeFold :: r -> (a -> r -> r) -> Fold a r
makeFold start step = Fold start' step' where
  start' = ((), start)
  step' a ((), r) = ((), step a r)
于 2012-10-18T15:50:00.647 回答
6

tl;博士：

结论1：你不能

你最初要求的东西是不可能的，至少不是你想要的任何版本我都能想出。（见下文。）如果更改您的数据类型以允许我存储中间计算，我想我会没事的，但即使那样，该功能unFold也会相当低效，这似乎与您聪明的优化技巧议程背道而驰！

结论 2：我认为它没有达到你想要的效果，即使你通过改变类型来解决它

列表算法的任何优化都会受到您使用原始未优化函数计算阶跃函数的问题的影响，而且很可能是以复杂的方式。

由于函数不相等，因此不可能将 step 优化为有效的东西。我认为你需要一个人来做unFold，而不是一个编译器。

无论如何，回到最初的问题：

可以折叠。展开 = 身份证？

不。假设我们有

isSingleton :: [a] -> Bool
isSingleton [x] = True
isSingleton _ = False

then if we have unFold :: ([x] -> y) -> Fold x ythen if与需要foldSingleton的相同unFold isSingleton

foldSingleton = Fold {start = False , step = ???}

其中 step 获取列表的一个元素并更新结果。现在isSingleton "a" == True，我们需要

step False = True

因为isSingleton "ab" == False，我们需要

step True = False

所以step = not到目前为止，isSingleton "abc" == False我们也需要

step False = False

因为有些函数([x] -> y)不能用类型的值表示Fold x y，所以不可能存在unFold :: ([x] -> y) -> Fold x y这样的函数fold . unFold = id，因为id是一个全函数。

编辑：

事实证明您对此并不信服，因为您只期望unFold处理具有折叠表示的函数，所以也许您的意思是unFold.fold = id.

可以展开。折叠 = 身份证？

不
，即使您只想unFold处理([x] -> y)可以使用 获得的功能fold :: Fold x y -> ([x] -> y)，我认为这是不可能的。让我们假设现在我们已经定义了这个问题

combine :: X -> Y -> Y
initial :: Y

folded :: [X] -> Y
folded = fold $ Fold initial combine

恢复价值initial是微不足道的：initial = folded []. 恢复原件combine不是，因为没有办法从一个给你一些值的函数Y到一个组合任意值的函数Y。

例如，如果我们有X = Y = Int并且我定义了

    combine x y | y < 0 = -10
                | otherwise = y + 1
    initial = 0

然后，因为每次在 positive 上使用它时都combine加一，并且初始值为 0，就其输出而言无法区分。请注意，由于永远不会是负数，因此也不可能定义一个可以恢复我们函数的函数。这归结为不是内射的事实。它携带不同的 type 值到相同的 type 值。yyfoldedlengthfolded xsunFold :: ([x] -> y) -> Fold x ycombinefoldFold x y[x] -> y

因此，我证明了两件事：if unFold :: ([x] -> y) -> Fold x ythen bothfold.unFold /= id和 now alsounFold.fold /= id

我打赌你也不相信这一点，因为你并不真正关心你是从 得到Fold 0 (\_ y -> y+1)还是Fold 0 combine从 回来unFold folded，因为它们在重折叠时具有相同的价值！让我们再次缩小球门柱。也许你想unFold在函数可以通过 获得的时候工作fold，并且你很高兴它不会给你不一致的答案，只要你再次折叠结果，你会得到相同的函数。我可以用下一个问题来总结一下：

可以折叠。展开。折叠=折叠？

即，您能否定义unFold这fold.unFold是可通过 获得的函数集的标识fold？

我真的相信这是不可能的，因为在step不保留有关子列表中间值的额外信息的情况下计算函数不是一个容易处理的问题。

假设我们有

unFold f = Fold {start = f [], step = recoverstep f}

我们需要

recoverstep f x1 initial == f [x1]

因此，如果有 x 的 Eq 实例（敲响警钟！），那么 recoverstep 必须具有与

recoverstep f x1 y | y == initial = f [x1]

我们也需要

recoverstep f x2 (f [x1]) == f [x1,x2]

所以如果 x 有一个 Eq 实例，那么 recoverstep 必须具有与

recoverstep f x2 y | y == (f [x1]) = f [x1,x2]

但这里有一个大问题：x1这个等式右边的变量是自由的。这意味着从逻辑上讲，除非我们已经知道在 x 上使用了什么值，否则我们无法判断阶跃函数在 x 上应该具有什么值。我们需要将 等的值存储f [x1]在f [x1,x2]Fold 数据类型中以使其工作，这就是为什么我们不能定义unFold. 如果您更改数据类型 Fold 以允许我们存储有关中间列表的信息，我可以看到它会起作用，但就目前而言，恢复上下文是不可能的。

于 2012-10-18T08:50:29.290 回答
1

与Dan 的回答类似，但使用的方法略有不同。我们没有将累加器与最终被丢弃的部分结果配对，而是添加了一个“后处理”函数，它将从累加器类型转换为最终结果。

相同的“作弊”unFold只是在后处理步骤中完成所有工作：

{-# LANGUAGE ExistentialQuantification #-}

data Fold a r = forall c. Fold
  { _start  :: c
  , _step   :: a -> c -> c
  , _result :: c -> r }

fold :: Fold a r -> [a] -> r
fold (Fold start step result) = result . foldr step start

unFold :: ([a] -> r) -> Fold a r
unFold f = Fold [] (:) f

makeFold :: r -> (a -> r -> r) -> Fold a r
makeFold start step = Fold start step id
于 2012-10-19T01:58:49.527 回答