Mfcttrf

I'm reading through Some Tricks for List Manipulation, and it contains the following:

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

What we can see here is that we have two continuations stacked on top
of each other. When this happens, they can often “cancel out”, like
so:

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

I don't understand how you "cancel out" stacked continuations to get from the top code block to the bottom one. What pattern do you look for to make this transformation, and why does it work?

A function f :: a -> b can be "disguised" inside double continuations as a function f' :: ((a -> r1) -> r2) -> ((b -> r1) -> r2).

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

obfuscate has the nice property that it respects function composition: you can prove that obfuscate f . obfuscate g === obfuscate (f . g) in a few steps. That means that you can frequently use this transformation to untangle double-continuation computations that compose obfuscated functions together by factoring the obfuscate out of the composition. This question is an example of such an untangling.

The f in the top code block is the obfuscated version of the f in the bottom block (more precisely, top f x is the obfuscated version of bottom f x). You can see this by noticing how top f applies the outer continuation to a function that transforms its input and then applies the whole thing to the inner continuation, just like in the body of obfuscate.

So we can start to untangle zipRev:

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

Since the action of foldr here is to compose a bunch of obfuscated functions with each other (and with an rightmost id, which we can leave on the right), we can factor the obfuscate to the outside of the whole fold:

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

Now apply the definition of obfuscate and simplify:

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!

Given a function

g :: a₁ -> a₂

we can lift it to a function on continuations, switching the order:

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

This transformation is a contravariant functor, which is to say that it interacts with function composition by switching its order:

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

We can lift the lifted function again in the same way to a function on stacked continuations, with the order switched back:

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

Stacking two contravariant functors gives us a (covariant) functor:

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

This is exactly the transformation being reversed in your example, with g = (y:ys, r) -> (ys, (x, y):r). This g is an endomorphism (a₁ = a₂), and the foldr is composing together a bunch of copies of it with various x. What we’re doing is replacing the composition of double-lifted functions with the double-lift of the composition of the functions, which is just an inductive application of the functor laws:

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