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 ?)

Methaemoglobin

also note that the paper uses ML (the language), which is strict. as for your Haskell code, see what happens if we change the last line in the first version to in (x == y && r, ys). – Udale

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.

Sundried

Answer 2

The CPS code (in the question's original version --- since edited by OP) seems faulty. Looks like it should be

      walk (x:xs) (_:_:ys) k  =  walk xs ys (\(z:zs) -> x == z && k zs)

The non-CPS code starts the comparisons from the middle, and does n `div` 2 comparisons, for a list of length n. It continues testing even if a mismatch is discovered, so, is "linear".

The CPS code exits right away in such a case because (False && undefined) == False holds; so is "non-linear". The two are not equivalent so the first doesn't say anything about the second.

As the other answer is saying, not calling the continuation amounts to throwing an exception in a code without continuations, what the paper's author apparently calls "the direct [i.e., non-CPS(?) --wn] style".

_{(I haven't read the paper).}

It isn't difficult at all to code the early-exiting solution in the "direct" style, by the way. We would just use the same turtle-and-hare trick to discover the halves while also building the first half in reverse, and then call and $ zipWith (==) first_half_reversed second_half in Haskell, or its equivalent short-circuiting direct recursive variant, in a strict language like e.g. Scheme.

Udale

indeed ! fixing it in the question. _ can't be abused – Methaemoglobin

or in non portable haskell specific code and $ (==) <$> first_half_reversed <*> second_half I suppose – Methaemoglobin

not without some ZipList noise. :) also, simpler code is often clearer. – Udale