> 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.