Write a term on the pure untyped lambda calculus that, when applied to a church-encoded list of numbers, returns it with its numbers sorted in ascending or descending order. Church lists and numbers must be encoded as folds for their usual ADTs:

-- Usual ADTs for Lists and Nats (in Haskell, for example)
data List a = Cons a (List a) | Nil
data Nat a  = Succ (Nat a) | Zero

-- Their respective folds are the λ-calculus representation used on this challenge
church_list = (λ c n . (c ... (c ... (c ... n))))
church_num  = (λ succ zero . (succ (succ (succ ... zero))))

Example input:

(λ cons nil .
    (cons (λ f x . (f x))                         -- 1
    (cons (λ f x . (f (f (f (f (f (f (f x)))))))) -- 7
    (cons (λ f x . (f (f x)))                     -- 2
    (cons (λ f x . (f (f (f x))))                 -- 3

Example output:

(λ cons nil . 
    (cons (λ f x . (f x))                         -- 1
    (cons (λ f x . (f (f x)))                     -- 2
    (cons (λ f x . (f (f (f x))))                 -- 3
    (cons (λ f x . (f (f (f (f (f (f (f x)))))))) -- 7

The score of a submission will be calculated as follows:

score(x)    = 1
score(λx.t) = score(t) + 1
score(t s)  = score(t) + score(s) + 1

Lowest score wins.

  • 7
    \$\begingroup\$ The linked page provides three different Church encodings for lists, and there's nothing to stop it from changing in the future. In order that the question be unambiguous, you will need to define the particular encoding you have in mind explicitly in the question. (It would also be advisable to define the encoding of the numbers). \$\endgroup\$ Aug 24, 2015 at 15:19
  • 1
    \$\begingroup\$ ascending or descending order -- why do we get to pick? \$\endgroup\$
    – lynn
    Aug 24, 2015 at 17:02
  • \$\begingroup\$ I just didn't find a reason to limit it. Why not? \$\endgroup\$
    – MaiaVictor
    Aug 24, 2015 at 17:07

3 Answers 3


I've managed to beat my own mark:

sort = λabcd.a(λef.f(λghi.g(λj.h(λkl.kj(ikl)))(hi))e(λgh.h))

There is a caveat, though - this term must receive an additional argument with the maximum size of naturals that are considered. For example, sort 4 [1,7,3,6,5] will return [1,3], ignoring anything above or equal 4. Of course, you could just give infinity (i.e., the Y-combinator):

sort = λbcd.(λfx.f(x x))(λfx.f(x x))(λef.f(λghi.g(λj.h(λkl.kj(ikl)))

And it would sort any list of natural numbers, but this term obviously doesn't have a normal form anymore.


121 characters / score 91

sort = λabc.a(λdefg.f(d(λhij.j(λkl.k(λmn.mhi)l)(h(λkl.l)i))

It is in normal form and could be made shorter by lifting common subexpressions.


Here's an implementation of an insertion sort:

let nil =       \f x.x in
let cons = \h t.\f x.f h (t f x) in
let 0 =       \f x.x in
let succ = \n.\f x.f (n f x) in
let None =    \a b.b in
let Some = \x.\a b.a x in
let pred = \n.n (\opt.opt (\m.Some(succ m)) (Some 0)) None in
let optpred = \opt.opt pred None in
let - = \m n.n optpred (Some m) in
let < = \m n.\trueval falseval.- m n (\diff.falseval) trueval in
let pair = \x y.\f.f x y in
let snd = \p.p (\x y.y) in
let insert = \n l.snd (l (\h recpair.recpair (\rawtail insertedtail.
  let rawlist = cons h rawtail in
    pair rawlist (< h n (cons h insertedtail) (cons n rawlist))))
  (pair nil (cons n nil))) in
\l.l insert nil

Here, pred n returns an element of option nat: pred 0 is None whereas pred (n+1) is Some n. Then, - m n returns an element of option nat which is Some (m-n) if m>=n or None if m<n; and < m n returns a boolean. Finally, insert uses an internal function returning a pair where f l = (l, insert n l) (a fairly typical method to get the tail of the list to get passed to the recursion along with the recursive value).

Now, some notes for future golfing work: actually nil, 0, None happen to be the same function formally (and it also appears in snd). Then, I would certainly consider doing beta reductions on the let statements (which is of course the usual syntactic sugar where let a = x in y means (\a.y)x and thus has score score(x) + score(y) + 2) to see in which cases doing so would reduce the score - which it most definitely would for the bindings that are only used once.

Then would come trickier things: for example, I just noticed that formally pred = pair (pair (\m.Some(succ m)) (Some 0)) None, optpred = pair pred None, - = \m.pair optpred (Some m), the sort function definition amounts to pair insert nil, etc. which could reduce the score slightly.

  • \$\begingroup\$ Please calculate your score and state it in the answer \$\endgroup\$
    – N. Virgo
    Jun 10, 2019 at 13:26

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.