[Math] lambda calculus and category theory

category-theorycomputer sciencelambda-calculuslogic

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?

Best Answer

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.