So, I have been learning about lambda calculus at university and it seems too abstract and theoretical for me.
Is lambda calculus used anywhere practically?
P.S. I tried searching Haskell compiler code for anything related to lambda calculus but couldn't find anything...
I highly disagree that the lambda calculus is too abstract and theoretical. The lambda calculus is far simpler than any other model of computation I know of. The only concept needed to understand what's going on is the concept of applying a function with a known definition to a value. Contrast the definition of the untyped lambda calculus with the definition of a Turing machine.
But that's not the question OP asked.
Some applications of lambda calculus include:
Lambda calculus was the first formalism of "computability" in which what is now known as the "halting problem" was proved undecidable (by Alonzo Church, who mentored the more famous Alan Turing).
Lambda calculus is used as the foundation for many of the most powerful and elegant programming languages, including Haskell and dialects of Lisp. Functional languages tend to be particularly friendly to lambda.
Even languages which originally rejected lambda have now come around - even C++ and Java now include syntax inspired by that of the lambda calculus. Almost every modern language has support for defining a function using lambda.
Cartesian closed categories are categories with a notion of "Cartesian product" and a notion of "exponential objects" (which are the analogue of the set $\{f : A \to B\}$). All Cartesian closed categories have models of the simply typed lambda calculus. This includes important categories like the category of Sets and the category of directed graphs as well as other, more advanced examples like categories of sheaves on a site, which are highly useful in algebraic geometry and related fields.
Other examples of a Cartesian Closed Category include any Heyting algebra, the algebras used to interpret (possibly non-classical) propositional logic. This is the origin of the "propositions as types" Curry-Howard-Lambek correspondence.
Simply typed lambda calculus is the "internal language" of these categories.
When researchers set out to prove that Rust's safety guarantees actually meant that all code with no Unsafe blocks was safe, they developed a variant of the lambda calculus to do it.
There are also variants of the lambda calculus which model safe parallel programming, linear types, and many other intriguing concepts which are making their way into modern languages. Researchers will develop variants of the lambda calculus to model the behaviour of real-world languages and then prove certain desirable properties hold about these versions of lambda calculus.
Partial combinatory algebras allow one to develop all kinds of interesting models of set theory which have computational semantics. The untyped lambda calculus is the language of PCAs and allows one to simply prove many results about them.
Homotopy Type Theory, and dependent type theory in general, is an extension of simply typed lambda calculus. It provides powerful tools for the study of homotopy theory and homotopy types. It also serves as a powerful new foundation of mathematics in its own right. It's one of the most fascinating new fields of study in math to emerge over the last 3 decades in my opinion.
Abstract Stone Duality is basically a lambda-calculus for topology. I don't know much about it, but it appears to provide a powerful set of tools for topology.
