True! I think pattern matching and the high-powered static type system really pull a lot of weight here, though. Haskell's types are a whole other dimension of domain modeling. You can encode algebraic data types as pure lambdas, but it's much less pleasant IMHO. (Laziness also bakes some common streaming patterns into the language core, which I find really nice, but it also makes it harder to totally understand what's going on sometimes, so it's a bit more of a toss-up.)

Point being, nobody wants to model their data structures as pure lambdas; even primitive integers are an addition on top of the lambda calculus.

> For an example of a non-trivial program

I don't think I'm taking the point you wanted me to from this program. It's under 30 lines, yet I'd need to pore over this for twice as many minutes to comprehend what it's doing. I can see the lambda abstractions and applications clear as day, but what they're doing I couldn't say. (The comments clearly say it's a universal binary LC interpreter, but we don't usually judge languages by their comments.)

EDIT: Right, okay, it's a submission to the the International Obfuscated C Code Contest. If it's obfuscated, then indeed, I'm not meant to comprehend it easily. Not sure that sells the lambda calculus.

Spoiler alert, but if you want a tutorial on understanding Tromp's calculus, then here's the readable version of his IOCCC entry with cryptograms and everything deciphered. https://justine.lol/lambda/

> You can encode algebraic data types as pure lambdas, but it's much less pleasant IMHO

Not that much less, since you can manually translate back your Haskell code to lambda calculus. E.g. your

    List a = Nil | Cons a (List a)

rewrites to

    let
      Nil = \n\c. n
      Cons = \x\y. \n\c. c x y
    in ...

Of course the type system is what helps you write correct Haskell code in the first place, so the untyped lambda calculus will be painful for debugging wrongly typed code.

> pure lambdas

Also, in lambda calcalus there is no recursion built-in. You have to build it yourself with the Y combinator.

Right; you just add definitions you need like

let Y = \f. (\x. x x) (\x. f (x x)) in program-using-Y

which is the slightly more legible version of

(\Y. program-using-Y) (\f. (\x. x x) (\x. f (x x))