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$
3
  • 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

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$

You must log in to answer this question.

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