Lazy lists with call-by-value reduction strategy

Question

I am currently writing lists with lazy semantics in the pure lambda-calculus with call-by-value reduction strategy.

I tried to construct pleasant to use and relatively efficient "lazy" functions on lists. As in the Church encoding I identify list with its right fold function, but with some differences. Here is nil and cons:

nil       = \_ _ z. z
cons x xs = \_ f z. f (\_. x) (\f' _. force xs f' z)

This representation of cons gives a simple way to get the tail of a list, which is O(1):

tail xs = \_ f z. force xs (\_ r. force (r f)) z

You just discard the first argument of f in cons and force the second after applying it to function f, which the tail function receives. But it brings some problems with foldr. Consider

cons (s z) (cons (s (s z)) nil) 

After call-by-value and full beta-reduction (it reduces a term to a readable form) it becomes

\_ f z. f (\_ s z. s z) (\f' _. f' (\_ s z. s (s z)) (\'f' _. z))

To fold this term with one function, e.g. plus, you need to wrap and replicate it a little:

(\x r. plus (force x) (force (r 
(\x r. plus (force x) (force (r _))))))

'_' means "there is no difference, what term to choose". Then you add a default value z and after call-by-value and full beta-reduction the whole term

force (cons (s z) (cons (s (s z)) nil))
    (\x r. plus (force x) (force (r 
    (\x r. plus (force x) (force (r _)))))) z

reduces to

\s z. s (s (s z))

foldr is the generalization of this idea and defined as

foldr f z xs = force xs (fix (\rec x r. f x (r rec))) z

For example

sum = foldr (\x r. plus (force x) (force r) z

"Wrapping and replicating" is defined by fix, which is Z-combinator:

fix f = (\x. f (\y. x x y)) (\x. f (\y. x x y))

Having the head and tail functions it's easy to define take:

take = fix (\take n xs. if (eq0 n) nil (ifNullNil xs
    (\xs. consC (\_. head xs) (take (pred n) (tail xs)))))

ifNullNil returns nil, if the null function (an emptiness test) returns true for its first argument, or applies the second to the first and wraps the result into the thunk otherwise:

ifNull    = \xs z f. if (null xs) z (\_. force (f xs))
ifNullNil = \xs. ifNull xs nil

consC receives a thunk instead of a value and defined as

consC = \x xs _ f z. f x (\f' _. force xs f' z);

Finally you can define infinite lists:

nats = fix (\rec n _. force (cons n (rec (s n)))) z

And compose them with usual functions on lists:

sum (take (s (s (s z))) (cons (s (s (s z))) nats))

It reduces to

\s z. s (s (s (s z)))

and equals to Haskell's

sum $ take 3 $ 3:[0..] -- 3 + 0 + 1 + 0 = 4

Edit2

You need an extra '_' in the arguments of cons because it allows you to compose ordinary functions with functions, that generate infinite lists. Consider

nats = fix (\rec n _. force (cons n (rec (s n)))) z

It reduces to

nats = \_. force (cons z (fix (\rec n _. force (cons n (rec (s n)))) (s z)))

So list, which cons receives, should be "forceable". So list, which cons produces, should be "forceable" too, because you want to compose conses.

So my question is: are there some sources, from where I can learn more about such a representation or a better representations, that allow you to write programms with lazy semantics in languages with eager evaluation, especially in the pure lambda-calculus?

Answer 1

Have a look at Wadler et al's How to add laziness to a strict language without even being odd. It presents a number of techniques (for Standard ML) and provides a good survey of the literature of the time.

The most naive way is to delay the evaluation of term $t$ by making it, using a term such as $\text{delay }t=\lambda ().t$, and to force the evaluation of such a term by applying it, using a term such as $\text{force }t=t~()$. For less naive/more systematic approaches, integrated into programming languages, read the paper.

Answer 2

This representation doesn't allow efficient lists deconstructing actually. While the tail function is O(1), every call to it increases the size of a term instead of decreasing. This leads to quadratic complexity for the zipWith function for example. Boehm-Berarducci encoding has the same problem. One another option is to represent a list as its right fold, but with passing an accumulator from left ro right. This approach is quite more readable, than Boehm-Berarducci encoding, but has the same problem with lists deconstructing.

Scott encoding solves the problem (this version doesn't contain explicit thunking):

nil          = \_ z. z
cons    x xs = \f z. f xs x (xs f z)
head    z xs = xs (\_ x _. x) z
tail      xs = xs (\xs' _ _. xs') nil
foldr f z xs = xs (\_. f) z

Emulating tagged unions also solves the problem.

Neither approach is nice. Pattern-matching mixed with normal-order reduction strategy is a bless.