15
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ One example might be the Curry-Howard-Lambek correspondence, see e.g. here and here. $\endgroup$ – dtldarek Dec 2 '13 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$ – Aleš Bizjak Dec 2 '13 at 8:10
  • 1
    $\begingroup$ This talk would be a very good answer to the question. $\endgroup$ – Bobby Marinoff May 2 '16 at 10:09
13
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.