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?

  • 2
    $\begingroup$ One example might be the Curry-Howard-Lambek correspondence, see e.g. here and here. $\endgroup$
    – dtldarek
    Dec 2, 2013 at 7:49
  • 2
    $\begingroup$ One should be careful here which "lambda calculus" one has in mind. Simply typed lambda calculus is the natural internal language of cartesian closed categories. Unityped (aka untyped) is not. $\endgroup$ Dec 2, 2013 at 8:10
  • 1
    $\begingroup$ This talk would be a very good answer to the question. $\endgroup$
    – Jencel
    May 2, 2016 at 10:09

1 Answer 1


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.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .