lambda calculus and category theory

logic computer-science category-theory lambda-calculus

I am not particularly knowledgeable in either lambda calculus or category theory, but I am starting to learn Haskell so I would like to ask: are there connections between category theory and lambda calculus? Could anyone describe those connections in layman's terms?


Every model of a typed lambda calculus is a cartesian closed category.

Every cartesian closed category can be expressed as a typed lambda calculus (with the objects as types and arrows as terms).

Thus, typed lambda calculus and cartesian closed category are essentially the same concept.

Related

A relation between product and quotient topology.
General method to "naturally interpolate" to a complex map?
Positive integer solutions to $x^4+y^7=z^9$
Uniform limit of uniformly continuous functions
An integral $\int^\infty_0\frac{\tanh{x}}{x(1-2\cosh{2x})^2}{\rm d}x$
(Co)homology theory and electrical circuit
How to obtain Grothendieck’s “Long March Through Galois Theory”
Are the addition and multiplication of real numbers, as we know them, unique?
Meaning of the inverse of the Laplacian matrix
Counter-examples related to Slutsky's Theorem.
What does it mean when a bound is sharp?
How thick should a cylindrical coin be for it to act as a fair three-sided die?