Perhaps this page is now superseded by the Mairson constructs.

Safalra shows some ways to do ‘ordinary code’ in the λ calculus. We repeat the stuff here.

Two truth values K = true = (λab.a) and H = false = (λab.b) play a double role. If x is a truth value then (x p q) evaluates to p if x=true and otherwise to q. Both values are calculated and this is usually bad. The construct (x (λd.p) (λe.p) i) evaluates only one of p or q and the other expression is unevaluated. The identifier d should not appear in p freely, nor e in q. The value of i is ignored but that ID must be in scope. The primordial zero test z produces either H or K and other predicates should as well.

The familiar LISP or Scheme value (cons x y) may be had by (λz.zxy). If c is such a value then (c K) is (car c) and (c H) is (cdr c). If you want car and cdr functions then (λx.xK) and (λx.xH) serve. We will also need a nil value and matching null? predicate.

Following Safalra we try the following:

pair = (λabf.fab)
first =  (λp.p(λab.a))
second = (λp.p(λab.b))
(first  (pair 3 5)) = ((λp.p(λab.a)) ((λabf.fab) 3 5)) => 3
(second (pair 3 5)) = ((λp.p(λab.b)) ((λabf.fab) 3 5)) => 5
This plan does not allow for lists of unknown length. For those Safalra proposes the following:
nil = (λfx.x)
cons = (λalfx.fa(lfx))
car = (λl.l(λab.a)i)
cdr = (λl. car (l(λab. cons (cdr b)(cons a (cdr b)))(cons nil nil)))
null? = (λl.l(λab.K)H)
Running these seems to require a nest of definitions; we use the second letter of each name as our ident:
((λioau.((λd.
42 ; app
)
(λl.a(l(λab.o(db)(oa(d b)))(oii)))))
(λfx.x)         ; i for nil
(λalfx.fa(lfx)) ; o for cons
(λl.l(λab.a)i)  ; a for car
(λl.l(λab.K)H)  ; u for null?
)
Reduction:
(cons 3 5) = ((λalfx.fa(lfx)) 3 5)
(car (cons 3 5)) = ((λl.l(λab.a)i) ((λalfx.fa(lfx)) 3 5)) => number as function
((λalfx.fa(lfx)) 3 5(λab.a)i)
((λlfx.f3(lfx)) 5 (λab.a)i)
((λfx.f3(5fx)) (λab.a)i)
((λfx.f3(5fx)) K i)
((λx.K3(5Kx)) i)
(K3(5Ki))
3 ; but with (5Ki) evaluated and discarded. Perhaps Safalra assumes lazy evaluation. I think that list semantics in the λ calculus should not allow calling a list element.