How can two continuations cancel each other out?

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 preserves function composition and identity: you can prove that obfuscate f . obfuscate g === obfuscate (f . g) and that obfuscate id === id 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 apply it all to 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!

Leave a Comment

tech