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


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?

  • $\begingroup$ Standard Church encoding with Boehm-Berarducci isomorphism is a much better approach. But a direct translation of it into the pure lambda-calculus is not as simple, as what I describe, though. $\endgroup$ Feb 14, 2014 at 19:03
  • $\begingroup$ Do I understand correctly? You've modified the question to include the answer? It would be better to just post the answer as an answer. $\endgroup$ Feb 15, 2014 at 21:52
  • $\begingroup$ No, I modified the question, because there was a bug in it. Questions are still the same: does this approach have a name and are there better approaches? $\endgroup$ Feb 15, 2014 at 21:55
  • 1
    $\begingroup$ The problem is that you modified your question so that the actual question is lost. It would be better to have a single coherent question, rather than a question followed by two edits, one of which contains another embedded question. The question should probably be at the top, or the bottom, or possible both, making note that you are repeating the question if you decide to take the final approach. $\endgroup$ Feb 16, 2014 at 6:49

2 Answers 2


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.

  • $\begingroup$ Thanks. It's actually not about pure lambda-calculus, but there is some useful terminology. $\endgroup$ Feb 14, 2014 at 0:02
  • $\begingroup$ If you squint hard enough, a programming language like Standard ML can be seen as syntactic sugar for the lambda calculus. $\endgroup$ Feb 16, 2014 at 6:49
  • $\begingroup$ It's a very sweet sugar. Implementing tagged unions in the pure lambda-calculus to emulate ml-like ADT's is not pleasant at all. $\endgroup$ Feb 16, 2014 at 10:20

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.