Palindrome and Danvy's remark on direct style

Question

Here is some code deciding whether a list is a palindrome in n+1 comparisons, in "direct style"

pal_d1 :: Eq a => [a] -> Bool
pal_d1 l = let (r,_) = walk l l in r
        where walk l           [] = (True,l) 
              walk l       (_:[]) = (True,tail l)
              walk (x:l) (_:_:xs) = let (r, y:ys) = walk l xs
                                    in (r && x == y, ys)      

which can be tested on a few example

-- >>> pal_d1 [1,2,1]
-- True

-- >>> pal_d1 [1,2,2,1]
-- True

-- >>> pal_d1 [1,2,3,4,2,1]
-- False

Danvy claims in "There and back again" there is no direct style solution without a control operator (right before 4.2) due to the non linear use of the continuation in CPS style solution below :

pal_cps1 :: Eq a => [a] -> Bool
pal_cps1 l = walk l l (\_ -> trace "called" True) 
    where 
          walk  l          []  k = k l
          walk  l       (_:[]) k = k (tail l)
          walk (x:xs) (_:_:ys) k = walk xs ys (\(r:rs) ->  x == r && k rs)          

How is the first code not contradicting this assertion ?

(and how is the continuation not used linearly ?)

Answer 1

He does not claim that there is no solution without a control operator.

The continuation is not used linearly and therefore mapping this program back to direct style requires a control operator.

The context of the paper is to study systematic transformations between direct style and CPS, and the claim of that paragraph is that going back from CPS is tricky if the continuation is used in fancy ways.

With some effort you can wrangle it back into a nice shape, but the question remains, how might a compiler do that automatically?

(and how is the continuation not used linearly ?)

In the paper, the continuation is on the right of andalso (&&) so it's discarded if the left operand is False.

In operational semantics, you can view the continuation as an evaluation context, and in that view discarding the continuation corresponds to throwing an exception. One can certainly do it, but the point is that this requires extra machinery in the source language.