函数 f :: a -> b 可以作为一个函数在双重连续体中“伪装” f' :: ((a -> r1) -> r2) -> ((b -> r1) -> r2) .

obfuscate :: (a -> b) -> ((a -> r1) -> r2) -> (b -> r1) -> r2
obfuscate f k2 k1 = k2 (k1 . f)

obfuscate 它有一个很好的特性,即它保留了函数的组成和身份:你可以证明这一点 obfuscate f . obfuscate g === obfuscate (f . g) 而且 obfuscate id === id 只需几步。这意味着您可以经常使用此转换来解开构成 混淆 d函数通过分解 混淆 在作文之外。这个问题就是这样一个解决问题的例子。

这个 f 在最上面的代码块中是 混淆 d版本的 F 在底部块中(更准确地说,是顶部 f x 是吗 混淆 底部的d版本 f x ).你可以通过观察顶部 F 将外部延拓应用于转换其输入的函数,然后将整个内容应用于内部延拓,就像在函数体中一样 混淆 .

所以我们可以开始解开 zipRev :

zipRev xs ys = foldr f id xs snd (ys,[])
  where
    f x = obfuscate (\(y:ys,r) -> (ys,(x,y):r))

自从 foldr 下面是一组 混淆 d函数相互作用(并将其全部应用于 id ,我们可以把它留在右边),我们可以考虑 混淆 在整个褶皱的外侧:

zipRev xs ys = obfuscate (\accum -> foldr f accum xs) id snd (ys,[])
  where
    f x (y:ys,r) = (ys,(x,y):r)

现在应用 混淆 并简化:

zipRev xs ys = obfuscate (\accum -> foldr f accum xs) id snd (ys,[]) 
zipRev xs ys = id (snd . (\accum -> foldr f accum xs)) (ys,[])
zipRev xs ys = snd (foldr f (ys,[]) xs)

QED!

给定一个函数

g :: a₁ -> a₂

我们可以把它提升到一个连续的函数,切换顺序:

lift g = (\c a₁ -> c (g a₁))
    :: (a₂ -> t) -> a₁ -> t

这个变换是一个逆变函子,也就是说,它通过切换其顺序与函数合成相互作用:

g₁ :: a₁ -> a₂
g₂ :: a₂ -> a₃

lift g₁ . lift g₂
== (\c₁ a₁ -> c₁ (g₁ a₁)) . (\c₂ a₂ -> c₂ (g₂ a₂))
== \c₂ a₁ -> (\a₂ -> c₂ (g₂ a₂)) (g₁ a₁)
== \c₂ a₁ -> c₂ (g₂ (g₁ a₁)) 
== lift (g₂ . g₁)
    :: (a₃ -> t) -> a₁ -> t

lift id
== (\c a₁ -> c a₁)
== id
    :: (a₁ -> t) -> a₁ -> t

我们可以用同样的方法将提升函数再次提升为叠加连续函数,并将顺序切换回:

lift (lift g)
== (\k c -> k ((\c a₁ -> c (g a₁)) c))
== (\k c -> k (\a₁ -> c (g a₁)))
    :: ((a₁ -> t) -> u) -> (a₂ -> t) -> u

将两个逆变函子叠加,我们得到一个(协变)函子:

lift (lift g₁) . lift (lift g₂)
== lift (lift g₂ . lift g₁)
== lift (lift (g₁ . g₂))
    :: ((a₁ -> t) -> u) -> (a₃ -> t) -> u

lift (lift id)
== lift id
== id
    :: ((a₁ -> t) -> u) -> (a₁ -> t) -> u

在你的例子中,这正是被逆转的转换 g = \(y:ys, r) -> (ys, (x, y):r) 这 g 是一种自同态( a₁ = a₂ ),以及 foldr 正在用各种各样的方式将它的一堆副本组合在一起 x 我们所做的是用函数组合的双提升代替双提升函数的组合,这只是对函子定律的归纳应用:

f :: x -> a₁ -> a₁
c :: (a₁ -> t) -> u
xs :: [x]

foldr (\x -> lift (lift (f x))) c xs
== lift (lift (\a₁ -> foldr f a₁ xs)) c
    :: (a₁ -> t) -> u

让我们试着从一个基本的角度来理解这段代码。有人想知道它到底有什么用?

zipRev xs ys = foldr f id xs snd (ys,[])
  where
     -- f x k c = k (\(y:ys, r) -> c (ys, (x,y):r))
        f x k c = k (g x c) 
     --         = (k . g x) c   -- so,
     -- f x k   =  k . g x

        g x   c       (y:ys, r) =  c (ys, (x,y):r)

这里我们用过 lambda lifting 恢复 g combinator .

那是因为 f x k = k . g x 是 k 去 左边 属于 x ,输入列表被转换为一个相反的合成链,

foldr f id [x1, x2, x3, ..., xn]   where  f x k = k . g x
  ===>> 
   (((...(id . g xn) .  ...  . g x3) . g x2) . g x1)

因此,它只是做了一个左折叠会做的事情,

zipRev [] ys = []
zipRev [x1, x2, x3, ..., xn] ys 
      = (id . g xn  .  ...  . g x3 . g x2 . g x1)  snd         (ys, [])
      = g xn (g xn1 (  ...  ( g x3 ( g x2 ( g x1   snd)))...)) (ys, [])
   where     ----c--------------------------------------------
        g x  c     (y:ys, r) = c (ys, (x,y):r)

所以我们去了最深处 xs 列表,然后我们回来消费 ys 从左到右(即自上而下)列出,然后从右到左返回 xs 列表(即自下而上)。这是直接编码为一个右折叠,带有严格的减速器,因此流动确实是从右到左的 xs .最底层的行动( snd )在链中,它是最后完成的,因此在新代码中它成为最顶层(仍然是最后完成的):

zipRev xs ys = snd (foldr h (ys,[]) xs)
  where
        h x        (y:ys, r) =   (ys, (x,y):r)

g x c 在原始代码中用作延续,带有 c 作为第二层的延续;但事实上,一直以来,它都是从右边开始的一个常规褶皱。

因此,它确实将颠倒的第一个列表与第二个列表分开。它也不安全;它遗漏了一个条款:

        g x  c     ([],   r) = c ([], r)        -- or just `r`
        g x  c     (y:ys, r) = c (ys, (x,y):r)

(更新:) duplode(和Joseph Sible)的答案对lambda提升有点不同,以一种更适合任务的方式。事情是这样的:

zipRev xs ys = foldr f id xs  snd (ys,[])
  where
     f x k c = k      (\((y:ys), r) -> c (ys, (x,y):r)) 
             = k (c . (\((y:ys), r) ->   (ys, (x,y):r)) )
             = k (c . g x)
     g x     =        (\((y:ys), r) ->   (ys, (x,y):r))
  {- f x k c = k ((. g x) c) = (k . (. g x)) c = (. (. g x)) k c
     f x     =                                   (. (. g x))     -}

那么

foldr f id  [ x1,            x2,    ... ,         xn      ]  snd  (ys,[]) =
  = ( (. (. g x1)) $ (. (. g x2)) $ ... $ (. (. g xn)) id )  snd  (ys,[])  -- 1,2...n
  = ( id . (. g xn) .  ...  . (. g x2)  .    (. g x1)     )  snd  (ys,[])  -- n...2,1
  =      ( snd . g x1 .    g x2   . ... .       g xn            ) (ys,[])  -- 1,2...n!
  =        snd $ g x1 $    g x2   $ ... $       g xn              (ys,[])
  =        snd $  foldr g (ys,[])  [x1, x2, ...,  xn      ]

简单。:)翻动两次根本不是翻动。

让我们从一些装饰性的调整开始:

-- Note that `g x` is an endomorphism.
g :: a -> ([b], [(a,b)]) -> ([b], [(a,b)])
g x ((y:ys),r) = (ys,(x,y):r)

zipRev xs ys = foldr f id xs snd (ys,[])
  where
    f x k = \c -> k (c . g x)

f 继续( c . g x )转到另一个函数( k “双重延续”, as user11228628 puts it ).

虽然我们可以合理地预期 F 随着折叠的进行,将以某种方式组成 g x 由列表中的元素组成的自同态,自同态的组成顺序可能不是很明显,所以我们最好通过几个步骤来确定:

-- x0 is the first element, x1 the second, etc.
f x0 k0 
\c -> k0 (c . g x0)
\c -> (f x1 k1) (c . g x0) -- k0 is the result of a fold step.
\c -> (\d -> k1 (d . g x1)) (c . g x0) -- Renaming a variable for clarity.
\c -> k1 (c . g x0 . g x1)
-- etc .
-- xa is the *last* element, xb the next-to-last, etc.
-- ka is the initial value passed to foldr.
\c -> (f xa ka) (c . g x0 . g x1 . . . g xb)
\c -> (\d -> ka (d . g xa)) (c . g x0 . g x1 . . . g xb)
\c -> ka (c . g x0 . g x1 . . . g xb . g xa)

ka ,传递给foldr的初始值为 id ,这让事情变得更简单:

foldr f id xs = \c -> c . g x0 . g x1 . . . g xa

既然我们对 c 争论转到 foldr f id xs 在用自同态进行后期合成时,我们不妨将其排除在外:

zipRev xs ys = (snd . foldr h id xs) (ys,[])
  where
    h x e = g x . e

注意我们是如何从 CGx 到 g x . e 。可以说,这是CPS在最初实施中的欺骗行为的附带影响。

最后一步是注意 h x e = g x . e 与我们将要做的完全一致 implement foldr in terms of foldMap for the Endo monoid .或者,更明确地说:

foldEndo g i xs = foldr g i xs  -- The goal is obtaining an Endo-like definition.

foldEndo _ i [] = i
foldEndo g i (x : xs) = g x (foldEndo g i xs)

foldEndo g i xs = go xs i
    where
    go [] = \j -> j
    go (x : xs) = \j -> g x (foldEndo g j xs)

foldEndo g i xs = go xs i
    where
    go [] = \j -> j
    go (x : xs) = \j -> g x (go xs j)

foldEndo g i xs = go xs i
    where
    go [] = id
    go (x : xs) = g x . go xs

foldEndo g i xs = go xs i
    where
    h x e = g x . e
    go [] = id
    go (x : xs) = h x (go xs)

foldEndo g i xs = go xs i
    where
    h x e = g x . e
    go xs = foldr h id xs

foldEndo g i xs = foldr h id xs i
    where
    h x e = g x . e

这最终让我们找到了我们想要的:

zipRev xs ys = snd (foldr g (ys,[]) xs)

user11228628's answer 让我明白了。以下是我在阅读时的一些见解,以及一些逐步的转变。

洞察力

• 续集不会直接抵消。它们最终只能被取消(通过减少测试版),因为有可能将它们排除在外。
• 你要寻找的模式是 \k c -> k (c . f) (或者如果你喜欢不可读的无点, (. (. f)) )无论如何 f (请注意 F 不是lambda的参数)。
• 像 duplode points out in a comment ,可以将连续传递式函数视为函子,以及 obfuscate 他们的定义是什么 fmap .
• 将这样的函数从 foldr 适用于任何可能是有效函数的函数 fmap .

从第一个代码块到第二个代码块的完整转换

zipRev xs ys = foldr f id xs snd (ys,[])
  where
    f x k c = k (\((y:ys),r) -> c (ys,(x,y):r))

拉 c 从lambda出来

zipRev xs ys = foldr f id xs snd (ys,[])
  where
    f x k c = k (c . \((y:ys),r) -> (ys,(x,y):r))

代替 混淆 因为它的定义

zipRev xs ys = foldr f id xs snd (ys,[])
  where
    f x = obfuscate (\((y:ys),r) -> (ys,(x,y):r))

拉 混淆 从lambda出来

zipRev xs ys = foldr f id xs snd (ys,[])
  where
    f = obfuscate . \x ((y:ys),r) -> (ys,(x,y):r)

拉 混淆 F

zipRev xs ys = foldr (obfuscate . f) id xs snd (ys,[])
  where
    f x ((y:ys),r) = (ys,(x,y):r)

自从 混淆 遵循函子定律,我们可以把它从 福尔德

zipRev xs ys = obfuscate (flip (foldr f) xs) id snd (ys,[])
  where
    f x ((y:ys),r) = (ys,(x,y):r)

内联 混淆

zipRev xs ys = (\k c -> k (c . flip (foldr f) xs)) id snd (ys,[])
  where
    f x ((y:ys),r) = (ys,(x,y):r)

β-减少

zipRev xs ys = (id (snd . flip (foldr f) xs)) (ys,[])
  where
    f x ((y:ys),r) = (ys,(x,y):r)

简化

zipRev xs ys = snd (foldr f (ys,[]) xs)
  where
    f x (y:ys,r) = (ys,(x,y):r)

拉取有效函数的理由 fmap 他不在 福尔德

foldr (fmap . f) z [x1,x2,...,xn]

扩展 福尔德

(fmap . f) x1 . (fmap . f) x2 . ... . (fmap . f) xn $ z

内线 . s

fmap (f x1) . fmap (f x2) . ... . fmap (f xn) $ z

应用函子定律

fmap (f x1 . f x2 . ... . f xn) $ z

展开括号中的部分

fmap (\z2 -> f x1 . f x2 . ... . f xn $ z2) z

写下lambda body的 福尔德

fmap (\z2 -> foldr f z2 [x1,x2,...,xn]) z

写下lambda body的 flip

fmap (flip (foldr f) [x1,x2,...,xn]) z

额外好处:证明拉取函数是有效的 contramap 他不在 福尔德

foldr (contramap . f) z [x1,x2,...,xn]

扩展 福尔德

(contramap . f) x1 . (contramap . f) x2 . ... . (contramap . f) xn $ z

内线 . s

contramap (f x1) . contramap (f x2) . ... . contramap (f xn) $ z

应用反变定律

contramap (f xn . ... . f x2 . f x1) $ z

展开括号中的部分

contramap (\z2 -> f xn . ... . f x2 . f x1 $ z2) z

写下lambda body的 福尔德

contramap (\z2 -> foldr f z2 [xn,...,x2,x1]) z

写下lambda body的 轻弹

contramap (flip (foldr f) [xn,...,x2,x1]) z

申请 foldr f z (reverse xs) = foldl (flip f) z xs

contramap (flip (foldl (flip f)) [x1,x2,...,xn]) z