How exactly is lambda calculus the foundation for functional programming languages? One of the question on usability of lambda calculus highlighted that lambda calculus is the foundation for programming languages, including Haskell and Lisp.
How is that exactly?
Do compilers in Haskell and Lisp actually implement lambda terms e.g. Church encodings?
I tried searching Haskell compiler code for anything related to lambda calculus but couldn't find anything...
 A: Welcome to MSE!
Lambda Calculus is horribly inefficient for modern computers, and so every programming language meant for use in the real world (this category includes both Haskell and Lisp) has a lot of functionality "baked in" (such as numeric and string literals, floats, etc) that the compiler can easily optimize to machine code. In particular, the church encoding of numerals is interesting theoretically (since it shows just how little lambda calculus you need in order to be turing complete), but is certainly not how real-world functional programming languages implement numbers.
The reason people say that Haskell, etc. are "based on lambda calculus" is because they are extensions of lambda calculus in a very precise way. For instance, in the default lambda calculus we have an extremely minimal grammar
$$
e ::= x \mid \lambda x. e \mid e_1 e_2
$$
as well as semantic rules for how these terms interact. The important one being
$$(\lambda x. e_1) e_2 \mapsto [e_2 / x] e_1$$
where we substitute $e_2$ for $x$ inside $e_1$.
You can imagine extending this to something more usable. Say, by adding numbers as a basic object, as well as the ability to add two expressions
$$
e ::= x \mid \lambda x . e \mid e_1 e_2 \mid \overline{n} \mid e_1 + e_2
$$
Of course, we need to define the semantics for these new symbols, and they might include rules like
$$
\overline{3} + \overline{7} \mapsto \overline{10}
$$
in general, the rule is (obviously)
$$
\overline{m} + \overline{n} \mapsto \overline{m+n}
$$
but that looks a little bit silly since we're overloading $+$.

Now you can imagine we keep extending the syntax for lambda calculus in this way, adding literals for strings, booleans, tuples, etc. Eventually, we'll have extended our way to a fully fledged programming language!
The only major language (though I do use that term loosely) which fully embraces this paradigm is sml, which has a full specification in this style, and has even had its type system proven safe. Other functional programming languages are informally based on the lambda calculus, but as far as I know they are not precisely specified in this way. This is unfortunate from a theoretical perspective, but really greases the wheels on a practical level, as it lets the maintainers introduce new features more easily.
If you want to read more about formal specifications for programming languages, I highly recommend Bob Harper's Practical Foundations for Programming Languages, much of which is freely available here (and all of which is freely available from websites of ill repute).
In it, many toy programming languages (of increasing complexity) are discussed, with their features, some implementation details, and techniques for proving various properties about these languages. It will give you a much deeper understanding of how functional languages are based in lambda calculus than I can possibly provide in this answer!

I hope this helps ^_^
